MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sban Structured version   Visualization version   Unicode version

Theorem sban 2248
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
StepHypRef Expression
1 sbn 2240 . . 3  |-  ( [ y  /  x ]  -.  ( ph  ->  -.  ps )  <->  -.  [ y  /  x ] ( ph  ->  -.  ps ) )
2 sbim 2244 . . . 4  |-  ( [ y  /  x ]
( ph  ->  -.  ps ) 
<->  ( [ y  /  x ] ph  ->  [ y  /  x ]  -.  ps ) )
3 sbn 2240 . . . . 5  |-  ( [ y  /  x ]  -.  ps  <->  -.  [ y  /  x ] ps )
43imbi2i 319 . . . 4  |-  ( ( [ y  /  x ] ph  ->  [ y  /  x ]  -.  ps ) 
<->  ( [ y  /  x ] ph  ->  -.  [ y  /  x ] ps ) )
52, 4bitri 257 . . 3  |-  ( [ y  /  x ]
( ph  ->  -.  ps ) 
<->  ( [ y  /  x ] ph  ->  -.  [ y  /  x ] ps ) )
61, 5xchbinx 317 . 2  |-  ( [ y  /  x ]  -.  ( ph  ->  -.  ps )  <->  -.  ( [
y  /  x ] ph  ->  -.  [ y  /  x ] ps )
)
7 df-an 378 . . 3  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
87sbbii 1812 . 2  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  [ y  /  x ]  -.  ( ph  ->  -.  ps ) )
9 df-an 378 . 2  |-  ( ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) 
<->  -.  ( [ y  /  x ] ph  ->  -.  [ y  /  x ] ps ) )
106, 8, 93bitr4i 285 1  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 376   [wsb 1805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-12 1950  ax-13 2104
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-ex 1672  df-nf 1676  df-sb 1806
This theorem is referenced by:  sb3an  2249  sbbi  2250  sbabel  2640  cbvreu  3003  sbcan  3298  rmo3  3344  inab  3702  difab  3703  exss  4663  inopab  4970  mo5f  28199  rmo3f  28210  iuninc  28253  suppss2fOLD  28313  suppss2f  28314  fmptdF  28331  disjdsct  28358  esumpfinvalf  28971  measiuns  29113  ballotlemodife  29403  sb5ALT  36952  sbcangOLD  36960  2uasbanh  36998  2uasbanhVD  37371  sb5ALTVD  37373  ellimcabssub0  37794
  Copyright terms: Public domain W3C validator