Theorem sban 1982

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 1912	. . . 4 |- ( [ z / x ] ( ph /\ ps ) <-> ( [ z / x ] ph /\ [ z / x ] ps ) )
2	1	sbbii 1787	. . 3 |- ( [ y / z ] [ z / x ] ( ph /\ ps ) <-> [ y / z ] ( [ z / x ] ph /\ [ z / x ] ps ) )
3		sbanv 1912	. . 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 1548	. . 3 |- ( ( ph /\ ps ) -> A. z ( ph /\ ps ) )
6	5	sbco2vh 1972	. 2 |- ( [ y / z ] [ z / x ] ( ph /\ ps ) <-> [ y / x ] ( ph /\ ps ) )
7		ax-17 1548	. . . 4 |- ( ph -> A. z ph )
8	7	sbco2vh 1972	. . 3 |- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )
9		ax-17 1548	. . . 4 |- ( ps -> A. z ps )
10	9	sbco2vh 1972	. . 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 1784

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785

This theorem is referenced by:  sb3an  1985  sbbi  1986  sbmo  2112  moanim  2127  sbabel  2374  nfrexdya  2541  cbvreu  2735  rmo3f  2969  sbcan  3040  sbcang  3041  rmo3  3089  inab  3440  difab  3441  exss  4270  inopab  4809  bdcriota  15752