Theorem sban 2006

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 1936	. . . 4 |- ( [ z / x ] ( ph /\ ps ) <-> ( [ z / x ] ph /\ [ z / x ] ps ) )
2	1	sbbii 1811	. . 3 |- ( [ y / z ] [ z / x ] ( ph /\ ps ) <-> [ y / z ] ( [ z / x ] ph /\ [ z / x ] ps ) )
3		sbanv 1936	. . 3 |- ( [ y / z ] ( [ z / x ] ph /\ [ z / x ] ps ) <-> ( [ y / z ] [ z / x ] ph /\ [ y / z ] [ z / x ] ps ) )
4	2, 3	bitri 184	. 2 |- ( [ y / z ] [ z / x ] ( ph /\ ps ) <-> ( [ y / z ] [ z / x ] ph /\ [ y / z ] [ z / x ] ps ) )
5		ax-17 1572	. . 3 |- ( ( ph /\ ps ) -> A. z ( ph /\ ps ) )
6	5	sbco2vh 1996	. 2 |- ( [ y / z ] [ z / x ] ( ph /\ ps ) <-> [ y / x ] ( ph /\ ps ) )
7		ax-17 1572	. . . 4 |- ( ph -> A. z ph )
8	7	sbco2vh 1996	. . 3 |- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )
9		ax-17 1572	. . . 4 |- ( ps -> A. z ps )
10	9	sbco2vh 1996	. . 3 |- ( [ y / z ] [ z / x ] ps <-> [ y / x ] ps )
11	8, 10	anbi12i 460	. 2 |- ( ( [ y / z ] [ z / x ] ph /\ [ y / z ] [ z / x ] ps ) <-> ( [ y / x ] ph /\ [ y / x ] ps ) )
12	4, 6, 11	3bitr3i 210	1 |- ( [ y / x ] ( ph /\ ps ) <-> ( [ y / x ] ph /\ [ y / x ] ps ) )

Syntax hints:   /\ wa 104   <-> wb 105   [wsb 1808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809

This theorem is referenced by:  sb3an  2009  sbbi  2010  sbmo  2137  moanim  2152  sbabel  2399  nfrexdya  2566  cbvreu  2763  rmo3f  3000  sbcan  3071  sbcang  3072  rmo3  3121  inab  3472  difab  3473  exss  4312  inopab  4853  bdcriota  16204