Metamath Proof Explorer

Theorem bj-dfbi6

Description: Alternate definition of the biconditional. (Contributed by BJ, 4-Oct-2019)

Ref Expression
Assertion bj-dfbi6 ⊢ φ ↔ ψ ↔ φ ∨ ψ ↔ φ ∧ ψ

Proof

Step Hyp Ref Expression
1 bj-dfbi5 ⊢ φ ↔ ψ ↔ φ ∨ ψ → φ ∧ ψ
2 id ⊢ φ ∨ ψ → φ ∧ ψ → φ ∨ ψ → φ ∧ ψ
3 animorr ⊢ φ ∧ ψ → φ ∨ ψ
4 2 3 impbid1 ⊢ φ ∨ ψ → φ ∧ ψ → φ ∨ ψ ↔ φ ∧ ψ
5 biimp ⊢ φ ∨ ψ ↔ φ ∧ ψ → φ ∨ ψ → φ ∧ ψ
6 4 5 impbii ⊢ φ ∨ ψ → φ ∧ ψ ↔ φ ∨ ψ ↔ φ ∧ ψ
7 1 6 bitri ⊢ φ ↔ ψ ↔ φ ∨ ψ ↔ φ ∧ ψ