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

Theorem sban 2011
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 2004 . . 3  |-  ( [ y  /  x ]  -.  ( ph  ->  -.  ps )  <->  -.  [ y  /  x ] ( ph  ->  -.  ps ) )
2 sbim 2007 . . . 4  |-  ( [ y  /  x ]
( ph  ->  -.  ps ) 
<->  ( [ y  /  x ] ph  ->  [ y  /  x ]  -.  ps ) )
3 sbn 2004 . . . . 5  |-  ( [ y  /  x ]  -.  ps  <->  -.  [ y  /  x ] ps )
43imbi2i 303 . . . 4  |-  ( ( [ y  /  x ] ph  ->  [ y  /  x ]  -.  ps ) 
<->  ( [ y  /  x ] ph  ->  -.  [ y  /  x ] ps ) )
52, 4bitri 240 . . 3  |-  ( [ y  /  x ]
( ph  ->  -.  ps ) 
<->  ( [ y  /  x ] ph  ->  -.  [ y  /  x ] ps ) )
61, 5xchbinx 301 . 2  |-  ( [ y  /  x ]  -.  ( ph  ->  -.  ps )  <->  -.  ( [
y  /  x ] ph  ->  -.  [ y  /  x ] ps )
)
7 df-an 360 . . 3  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
87sbbii 1636 . 2  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  [ y  /  x ]  -.  ( ph  ->  -.  ps ) )
9 df-an 360 . 2  |-  ( ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) 
<->  -.  ( [ y  /  x ] ph  ->  -.  [ y  /  x ] ps ) )
106, 8, 93bitr4i 268 1  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358   [wsb 1631
This theorem is referenced by:  sb3an  2012  sbbi  2013  sbabel  2447  cbvreu  2764  sbcan  3035  sbcang  3036  rmo3  3080  inab  3438  difab  3439  exss  4238  inopab  4818  ballotlemodife  23058  mo5f  23145  iuninc  23160  rmo3f  23180  suppss2f  23203  fmptdF  23223  disjdsct  23371  esumpfinvalf  23446  measiuns  23546  sb5ALT  28344  2uasbanh  28383  2uasbanhVD  28760  sb5ALTVD  28762
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632
  Copyright terms: Public domain W3C validator