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

Theorem pm5.32 619
Description: Distribution of implication over biconditional. Theorem *5.32 of [WhiteheadRussell] p. 125. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
pm5.32  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( ( ph  /\ 
ps )  <->  ( ph  /\ 
ch ) ) )

Proof of Theorem pm5.32
StepHypRef Expression
1 notbi 288 . . . 4  |-  ( ( ps  <->  ch )  <->  ( -.  ps 
<->  -.  ch ) )
21imbi2i 305 . . 3  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( ph  ->  ( -.  ps  <->  -.  ch )
) )
3 pm5.74 237 . . 3  |-  ( (
ph  ->  ( -.  ps  <->  -. 
ch ) )  <->  ( ( ph  ->  -.  ps )  <->  (
ph  ->  -.  ch )
) )
4 notbi 288 . . 3  |-  ( ( ( ph  ->  -.  ps )  <->  ( ph  ->  -. 
ch ) )  <->  ( -.  ( ph  ->  -.  ps )  <->  -.  ( ph  ->  -.  ch ) ) )
52, 3, 43bitri 264 . 2  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( -.  ( ph  ->  -.  ps )  <->  -.  ( ph  ->  -.  ch ) ) )
6 df-an 362 . . 3  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
7 df-an 362 . . 3  |-  ( (
ph  /\  ch )  <->  -.  ( ph  ->  -.  ch ) )
86, 7bibi12i 308 . 2  |-  ( ( ( ph  /\  ps ) 
<->  ( ph  /\  ch ) )  <->  ( -.  ( ph  ->  -.  ps )  <->  -.  ( ph  ->  -.  ch ) ) )
95, 8bitr4i 245 1  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( ( ph  /\ 
ps )  <->  ( ph  /\ 
ch ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  pm5.32i  620  pm5.32d  622  xordi  867  cbval2OLD  1991  cbvex2  1992  rabbi  2888  rabxfrd  4746  asymref  5252  mpt22eqb  6181  dvdslelem  12896  cfilucfil4OLD  19275  cfilucfil4  19276  2sb5nd  28709  2sb5ndVD  29084  2sb5ndALT  29106  cbval2OLD7  29792  cbvex2OLD7  29793
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator