This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bianbi

Description: Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, 31-Jul-2023)

Ref Expression
Hypotheses bianbi.1 ⊢ φ ↔ ψ ∧ χ
bianbi.2 ⊢ ψ ↔ θ
Assertion bianbi ⊢ φ ↔ θ ∧ χ

Proof

Step Hyp Ref Expression
1 bianbi.1 ⊢ φ ↔ ψ ∧ χ
2 bianbi.2 ⊢ ψ ↔ θ
3 2 anbi1i ⊢ ψ ∧ χ ↔ θ ∧ χ
4 1 3 bitri ⊢ φ ↔ θ ∧ χ