Metamath Proof Explorer

Theorem sban

Description: Conjunction inside and outside of a substitution are equivalent. Compare 19.26 . (Contributed by NM, 14-May-1993) (Proof shortened by Steven Nguyen, 13-Aug-2023)

Ref Expression
Assertion sban ⊢ y x φ ∧ ψ ↔ y x φ ∧ y x ψ

Proof

Step Hyp Ref Expression
1 simpl ⊢ φ ∧ ψ → φ
2 1 sbimi ⊢ y x φ ∧ ψ → y x φ
3 simpr ⊢ φ ∧ ψ → ψ
4 3 sbimi ⊢ y x φ ∧ ψ → y x ψ
5 2 4 jca ⊢ y x φ ∧ ψ → y x φ ∧ y x ψ
6 pm3.2 ⊢ φ → ψ → φ ∧ ψ
7 6 sb2imi ⊢ y x φ → y x ψ → y x φ ∧ ψ
8 7 imp ⊢ y x φ ∧ y x ψ → y x φ ∧ ψ
9 5 8 impbii ⊢ y x φ ∧ ψ ↔ y x φ ∧ y x ψ