Theorem sban 1942

Description: Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)

Assertion

Ref	Expression
sban	|- ( [ y / x ] ( ph /\ ps ) <-> ( [ y / x ] ph /\ [ y / x ] ps ) )

Proof of Theorem sban

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sbanv 1876	. . . 4 |- ( [ z / x ] ( ph /\ ps ) <-> ( [ z / x ] ph /\ [ z / x ] ps ) )
2	1	sbbii 1752	. . 3 |- ( [ y / z ] [ z / x ] ( ph /\ ps ) <-> [ y / z ] ( [ z / x ] ph /\ [ z / x ] ps ) )
3		sbanv 1876	. . 3 |- ( [ y / z ] ( [ z / x ] ph /\ [ z / x ] ps ) <-> ( [ y / z ] [ z / x ] ph /\ [ y / z ] [ z / x ] ps ) )
4	2, 3	bitri 183	. 2 |- ( [ y / z ] [ z / x ] ( ph /\ ps ) <-> ( [ y / z ] [ z / x ] ph /\ [ y / z ] [ z / x ] ps ) )
5		ax-17 1513	. . 3 |- ( ( ph /\ ps ) -> A. z ( ph /\ ps ) )
6	5	sbco2vh 1932	. 2 |- ( [ y / z ] [ z / x ] ( ph /\ ps ) <-> [ y / x ] ( ph /\ ps ) )
7		ax-17 1513	. . . 4 |- ( ph -> A. z ph )
8	7	sbco2vh 1932	. . 3 |- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )
9		ax-17 1513	. . . 4 |- ( ps -> A. z ps )
10	9	sbco2vh 1932	. . 3 |- ( [ y / z ] [ z / x ] ps <-> [ y / x ] ps )
11	8, 10	anbi12i 456	. 2 |- ( ( [ y / z ] [ z / x ] ph /\ [ y / z ] [ z / x ] ps ) <-> ( [ y / x ] ph /\ [ y / x ] ps ) )
12	4, 6, 11	3bitr3i 209	1 |- ( [ y / x ] ( ph /\ ps ) <-> ( [ y / x ] ph /\ [ y / x ] ps ) )

Syntax hints:   /\ wa 103   <-> wb 104   [wsb 1749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750

This theorem is referenced by:  sb3an  1945  sbbi  1946  sbmo  2072  moanim  2087  sbabel  2333  nfrexdya  2500  cbvreu  2687  rmo3f  2918  sbcan  2988  sbcang  2989  rmo3  3037  inab  3385  difab  3386  exss  4199  inopab  4730  bdcriota  13600