Theorem sban 1928

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 1861	. . . 4 |- ( [ z / x ] ( ph /\ ps ) <-> ( [ z / x ] ph /\ [ z / x ] ps ) )
2	1	sbbii 1738	. . 3 |- ( [ y / z ] [ z / x ] ( ph /\ ps ) <-> [ y / z ] ( [ z / x ] ph /\ [ z / x ] ps ) )
3		sbanv 1861	. . 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 1506	. . 3 |- ( ( ph /\ ps ) -> A. z ( ph /\ ps ) )
6	5	sbco2vh 1918	. 2 |- ( [ y / z ] [ z / x ] ( ph /\ ps ) <-> [ y / x ] ( ph /\ ps ) )
7		ax-17 1506	. . . 4 |- ( ph -> A. z ph )
8	7	sbco2vh 1918	. . 3 |- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )
9		ax-17 1506	. . . 4 |- ( ps -> A. z ps )
10	9	sbco2vh 1918	. . 3 |- ( [ y / z ] [ z / x ] ps <-> [ y / x ] ps )
11	8, 10	anbi12i 455	. 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 1735

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736

This theorem is referenced by:  sb3an  1931  sbbi  1932  sbmo  2058  moanim  2073  sbabel  2307  nfrexdya  2470  cbvreu  2652  rmo3f  2881  sbcan  2951  sbcang  2952  rmo3  3000  inab  3344  difab  3345  exss  4149  inopab  4671  bdcriota  13081