Metamath Proof Explorer

Theorem bj-animbi

Description: Conjunction in terms of implication and biconditional. Note that the proof is intuitionistic (use of ax-3 comes from the unusual definition of the biconditional in set.mm). (Contributed by BJ, 23-Sep-2023)

Ref Expression
Assertion bj-animbi ⊢ φ ∧ ψ ↔ φ ↔ φ → ψ

Proof

Step Hyp Ref Expression
1 simpl ⊢ φ ∧ ψ → φ
2 pm3.4 ⊢ φ ∧ ψ → φ → ψ
3 1 2 2thd ⊢ φ ∧ ψ → φ ↔ φ → ψ
4 biimp ⊢ φ ↔ φ → ψ → φ → φ → ψ
5 4 pm2.43d ⊢ φ ↔ φ → ψ → φ → ψ
6 biimpr ⊢ φ ↔ φ → ψ → φ → ψ → φ
7 5 6 mpd ⊢ φ ↔ φ → ψ → φ
8 7 5 jcai ⊢ φ ↔ φ → ψ → φ ∧ ψ
9 3 8 impbii ⊢ φ ∧ ψ ↔ φ ↔ φ → ψ