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

Theorem sban 2104
Description: Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
sban  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) )

Proof of Theorem sban
StepHypRef Expression
1 sbn 2097 . . 3  |-  ( [ y  /  x ]  -.  ( ph  ->  -.  ps )  <->  -.  [ y  /  x ] ( ph  ->  -.  ps ) )
2 sbim 2100 . . . 4  |-  ( [ y  /  x ]
( ph  ->  -.  ps ) 
<->  ( [ y  /  x ] ph  ->  [ y  /  x ]  -.  ps ) )
3 sbn 2097 . . . . 5  |-  ( [ y  /  x ]  -.  ps  <->  -.  [ y  /  x ] ps )
43imbi2i 304 . . . 4  |-  ( ( [ y  /  x ] ph  ->  [ y  /  x ]  -.  ps ) 
<->  ( [ y  /  x ] ph  ->  -.  [ y  /  x ] ps ) )
52, 4bitri 241 . . 3  |-  ( [ y  /  x ]
( ph  ->  -.  ps ) 
<->  ( [ y  /  x ] ph  ->  -.  [ y  /  x ] ps ) )
61, 5xchbinx 302 . 2  |-  ( [ y  /  x ]  -.  ( ph  ->  -.  ps )  <->  -.  ( [
y  /  x ] ph  ->  -.  [ y  /  x ] ps )
)
7 df-an 361 . . 3  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
87sbbii 1660 . 2  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  [ y  /  x ]  -.  ( ph  ->  -.  ps ) )
9 df-an 361 . 2  |-  ( ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) 
<->  -.  ( [ y  /  x ] ph  ->  -.  [ y  /  x ] ps ) )
106, 8, 93bitr4i 269 1  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359   [wsb 1655
This theorem is referenced by:  sb3an  2105  sbbi  2106  sbabel  2551  cbvreu  2875  sbcan  3148  sbcang  3149  rmo3  3193  inab  3554  difab  3555  exss  4369  inopab  4947  mo5f  23818  rmo3f  23828  iuninc  23857  suppss2f  23894  fmptdF  23913  disjdsct  23933  esumpfinvalf  24264  measiuns  24367  ballotlemodife  24536  sb5ALT  27954  2uasbanh  27993  2uasbanhVD  28366  sb5ALTVD  28368
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656
  Copyright terms: Public domain W3C validator