Theorem sban 2399

Description: Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.)

Assertion

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

Proof of Theorem sban

Step	Hyp	Ref	Expression
1		sbn 2391	. . 3 |- ( [ y / x ] -. ( ph -> -. ps ) <-> -. [ y / x ] ( ph -> -. ps ) )
2		sbim 2395	. . . 4 |- ( [ y / x ] ( ph -> -. ps ) <-> ( [ y / x ] ph -> [ y / x ] -. ps ) )
3		sbn 2391	. . . . 5 |- ( [ y / x ] -. ps <-> -. [ y / x ] ps )
4	3	imbi2i 326	. . . 4 |- ( ( [ y / x ] ph -> [ y / x ] -. ps ) <-> ( [ y / x ] ph -> -. [ y / x ] ps ) )
5	2, 4	bitri 264	. . 3 |- ( [ y / x ] ( ph -> -. ps ) <-> ( [ y / x ] ph -> -. [ y / x ] ps ) )
6	1, 5	xchbinx 324	. 2 |- ( [ y / x ] -. ( ph -> -. ps ) <-> -. ( [ y / x ] ph -> -. [ y / x ] ps ) )
7		df-an 386	. . 3 |- ( ( ph /\ ps ) <-> -. ( ph -> -. ps ) )
8	7	sbbii 1887	. 2 |- ( [ y / x ] ( ph /\ ps ) <-> [ y / x ] -. ( ph -> -. ps ) )
9		df-an 386	. 2 |- ( ( [ y / x ] ph /\ [ y / x ] ps ) <-> -. ( [ y / x ] ph -> -. [ y / x ] ps ) )
10	6, 8, 9	3bitr4i 292	1 |- ( [ y / x ] ( ph /\ ps ) <-> ( [ y / x ] ph /\ [ y / x ] ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   [wsb 1880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-sb 1881

This theorem is referenced by:  sb3an  2400  sbbi  2401  sbabel  2793  cbvreu  3169  sbcan  3478  rmo3  3528  inab  3895  difab  3896  exss  4931  inopab  5252  mo5f  29324  rmo3f  29335  iuninc  29379  suppss2f  29439  fmptdF  29456  disjdsct  29480  esumpfinvalf  30138  measiuns  30280  ballotlemodife  30559  sb5ALT  38731  sbcangOLD  38739  2uasbanh  38777  2uasbanhVD  39147  sb5ALTVD  39149  ellimcabssub0  39849