Biconditional introduction

Biconditional introduction is a rule of inference that derives a biconditional when each statement has been shown to imply the other.

Conditional proof: A proof method that assumes an antecedent temporarily and derives a consequent to establish a conditional. Each direction needed for introduction can be established by a separate conditional proof.
Material conditional: A truth-functional connective that is false only when its antecedent is true and its consequent false. In classical logic, each direction used by the rule can be represented with this connective.
Biconditional elimination: A rule of inference that derives either direction of a conditional from a biconditional. Unlike introduction, it starts with the biconditional and derives a direction.
Propositional calculus: A formal system for reasoning about propositions and connectives such as negation, conjunction, and implication. Biconditional introduction is used to prove equivalences in this logical system.
Natural deduction: A formal proof system that derives conclusions from premises using explicit inference and introduction rules. Biconditional introduction is one rule within natural-deduction systems.
Logical equivalence: A relation between propositions that have the same truth value under every interpretation. The two conditional directions together express equivalence in classical propositional logic.
Material implication: The classical equivalence between a conditional and a disjunction containing the negated antecedent. This equivalence can transform a conditional, but does not itself prove both directions.
Logical equivalence proof: A derivation establishing that two expressions entail one another or have identical truth conditions. The rule packages two directional derivations into one biconditional conclusion.
Subproof: A delimited section of a formal proof in which assumptions support an intermediate derivation. The two conditional derivations commonly use separate subproofs before the biconditional is introduced.
Proposition: A declarative statement capable of being true or false. The rule combines two propositions into a biconditional claim.

Linked from 2 pages

Conjunction introductionCompared with: It requires two conditional proofs rather than two propositions as direct premises.