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 yxφψyxφyxψ

Proof

Step Hyp Ref Expression
1 simpl φψφ
2 1 sbimi yxφψyxφ
3 simpr φψψ
4 3 sbimi yxφψyxψ
5 2 4 jca yxφψyxφyxψ
6 pm3.2 φψφψ
7 6 sb2imi yxφyxψyxφψ
8 7 imp yxφyxψyxφψ
9 5 8 impbii yxφψyxφyxψ