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 ] ( ph /\ ps ) <-> ( [ y / x ] ph /\ [ y / x ] ps ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( ph /\ ps ) -> ph )
2	1	sbimi	|- ( [ y / x ] ( ph /\ ps ) -> [ y / x ] ph )
3		simpr	|- ( ( ph /\ ps ) -> ps )
4	3	sbimi	|- ( [ y / x ] ( ph /\ ps ) -> [ y / x ] ps )
5	2 4	jca	|- ( [ y / x ] ( ph /\ ps ) -> ( [ y / x ] ph /\ [ y / x ] ps ) )
6		pm3.2	|- ( ph -> ( ps -> ( ph /\ ps ) ) )
7	6	sb2imi	|- ( [ y / x ] ph -> ( [ y / x ] ps -> [ y / x ] ( ph /\ ps ) ) )
8	7	imp	|- ( ( [ y / x ] ph /\ [ y / x ] ps ) -> [ y / x ] ( ph /\ ps ) )
9	5 8	impbii	|- ( [ y / x ] ( ph /\ ps ) <-> ( [ y / x ] ph /\ [ y / x ] ps ) )