Theorem sban 1971

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 1901	. . . 4 |- ( [ z / x ] ( ph /\ ps ) <-> ( [ z / x ] ph /\ [ z / x ] ps ) )
2	1	sbbii 1776	. . 3 |- ( [ y / z ] [ z / x ] ( ph /\ ps ) <-> [ y / z ] ( [ z / x ] ph /\ [ z / x ] ps ) )
3		sbanv 1901	. . 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 1537	. . 3 |- ( ( ph /\ ps ) -> A. z ( ph /\ ps ) )
6	5	sbco2vh 1961	. 2 |- ( [ y / z ] [ z / x ] ( ph /\ ps ) <-> [ y / x ] ( ph /\ ps ) )
7		ax-17 1537	. . . 4 |- ( ph -> A. z ph )
8	7	sbco2vh 1961	. . 3 |- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )
9		ax-17 1537	. . . 4 |- ( ps -> A. z ps )
10	9	sbco2vh 1961	. . 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 1773

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774

This theorem is referenced by:  sb3an  1974  sbbi  1975  sbmo  2101  moanim  2116  sbabel  2363  nfrexdya  2530  cbvreu  2724  rmo3f  2957  sbcan  3028  sbcang  3029  rmo3  3077  inab  3427  difab  3428  exss  4256  inopab  4794  bdcriota  15375