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

Theorem sban 1962
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 1955 . . 3  |-  ( [ y  /  x ]  -.  ( ph  ->  -.  ps )  <->  -.  [ y  /  x ] ( ph  ->  -.  ps ) )
2 sbim 1958 . . . 4  |-  ( [ y  /  x ]
( ph  ->  -.  ps ) 
<->  ( [ y  /  x ] ph  ->  [ y  /  x ]  -.  ps ) )
3 sbn 1955 . . . . 5  |-  ( [ y  /  x ]  -.  ps  <->  -.  [ y  /  x ] ps )
43imbi2i 305 . . . 4  |-  ( ( [ y  /  x ] ph  ->  [ y  /  x ]  -.  ps ) 
<->  ( [ y  /  x ] ph  ->  -.  [ y  /  x ] ps ) )
52, 4bitri 242 . . 3  |-  ( [ y  /  x ]
( ph  ->  -.  ps ) 
<->  ( [ y  /  x ] ph  ->  -.  [ y  /  x ] ps ) )
61, 5xchbinx 303 . 2  |-  ( [ y  /  x ]  -.  ( ph  ->  -.  ps )  <->  -.  ( [
y  /  x ] ph  ->  -.  [ y  /  x ] ps )
)
7 df-an 362 . . 3  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
87sbbii 1886 . 2  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  [ y  /  x ]  -.  ( ph  ->  -.  ps ) )
9 df-an 362 . 2  |-  ( ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) 
<->  -.  ( [ y  /  x ] ph  ->  -.  [ y  /  x ] ps ) )
106, 8, 93bitr4i 270 1  |-  ( [ y  /  x ]
( ph  /\  ps )  <->  ( [ y  /  x ] ph  /\  [ y  /  x ] ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    /\ wa 360   [wsb 1883
This theorem is referenced by:  sb3an  1963  sbbi  1964  sbabel  2420  cbvreu  2737  sbcan  3008  sbcang  3009  rmo3  3053  inab  3411  difab  3412  exss  4208  inopab  4804  ballotlemodife  23018  sb5ALT  27424  2uasbanh  27463  2uasbanhVD  27820  sb5ALTVD  27822
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884
  Copyright terms: Public domain W3C validator