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

Theorem sban 2191
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 2183 . . 3  |-  ( [ y  /  x ]  -.  ( ph  ->  -.  ps )  <->  -.  [ y  /  x ] ( ph  ->  -.  ps ) )
2 sbim 2187 . . . 4  |-  ( [ y  /  x ]
( ph  ->  -.  ps ) 
<->  ( [ y  /  x ] ph  ->  [ y  /  x ]  -.  ps ) )
3 sbn 2183 . . . . 5  |-  ( [ y  /  x ]  -.  ps  <->  -.  [ y  /  x ] ps )
43imbi2i 313 . . . 4  |-  ( ( [ y  /  x ] ph  ->  [ y  /  x ]  -.  ps ) 
<->  ( [ y  /  x ] ph  ->  -.  [ y  /  x ] ps ) )
52, 4bitri 252 . . 3  |-  ( [ y  /  x ]
( ph  ->  -.  ps ) 
<->  ( [ y  /  x ] ph  ->  -.  [ y  /  x ] ps ) )
61, 5xchbinx 311 . 2  |-  ( [ y  /  x ]  -.  ( ph  ->  -.  ps )  <->  -.  ( [
y  /  x ] ph  ->  -.  [ y  /  x ] ps )
)
7 df-an 372 . . 3  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
87sbbii 1793 . 2  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  [ y  /  x ]  -.  ( ph  ->  -.  ps ) )
9 df-an 372 . 2  |-  ( ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) 
<->  -.  ( [ y  /  x ] ph  ->  -.  [ y  /  x ] ps ) )
106, 8, 93bitr4i 280 1  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370   [wsb 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-12 1904  ax-13 2052
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-ex 1660  df-nf 1664  df-sb 1787
This theorem is referenced by:  sb3an  2192  sbbi  2193  sbabel  2614  sbabelOLD  2615  cbvreu  3051  sbcan  3339  rmo3  3387  inab  3738  difab  3739  exss  4677  inopab  4977  mo5f  28096  rmo3f  28107  iuninc  28156  suppss2fOLD  28218  suppss2f  28219  fmptdF  28236  disjdsct  28264  esumpfinvalf  28886  measiuns  29028  ballotlemodife  29319  sb5ALT  36734  sbcangOLD  36742  2uasbanh  36780  2uasbanhVD  37163  sb5ALTVD  37165  ellimcabssub0  37484
  Copyright terms: Public domain W3C validator