Metamath Proof Explorer

Theorem sb3an

Description: Threefold conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-Dec-2006)

Ref Expression
Assertion sb3an ⊢ y x φ ∧ ψ ∧ χ ↔ y x φ ∧ y x ψ ∧ y x χ

Proof

Step Hyp Ref Expression
1 df-3an ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ
2 1 sbbii ⊢ y x φ ∧ ψ ∧ χ ↔ y x φ ∧ ψ ∧ χ
3 sban ⊢ y x φ ∧ ψ ∧ χ ↔ y x φ ∧ ψ ∧ y x χ
4 sban ⊢ y x φ ∧ ψ ↔ y x φ ∧ y x ψ
5 4 anbi1i ⊢ y x φ ∧ ψ ∧ y x χ ↔ y x φ ∧ y x ψ ∧ y x χ
6 df-3an ⊢ y x φ ∧ y x ψ ∧ y x χ ↔ y x φ ∧ y x ψ ∧ y x χ
7 5 6 bitr4i ⊢ y x φ ∧ ψ ∧ y x χ ↔ y x φ ∧ y x ψ ∧ y x χ
8 2 3 7 3bitri ⊢ y x φ ∧ ψ ∧ χ ↔ y x φ ∧ y x ψ ∧ y x χ