Metamath Proof Explorer

Theorem abab

Description: Introduce one conjunct as equivalent to the other. "abab" stands for "and, biconditional, and, biconditional". (Contributed by Wolf Lammen, 4-Jun-2026)

Ref Expression
Assertion abab ⊢ φ ∧ ψ ↔ φ ∧ φ ↔ ψ

Proof

Step Hyp Ref Expression
1 simpl ⊢ φ ∧ ψ → φ
2 pm5.1 ⊢ φ ∧ ψ → φ ↔ ψ
3 1 2 jca ⊢ φ ∧ ψ → φ ∧ φ ↔ ψ
4 biimp ⊢ φ ↔ ψ → φ → ψ
5 4 anim2i ⊢ φ ∧ φ ↔ ψ → φ ∧ φ → ψ
6 abai ⊢ φ ∧ ψ ↔ φ ∧ φ → ψ
7 5 6 sylibr ⊢ φ ∧ φ ↔ ψ → φ ∧ ψ
8 3 7 impbii ⊢ φ ∧ ψ ↔ φ ∧ φ ↔ ψ