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

Theorem pm5.32 618
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 287 . . . 4  |-  ( ( ps  <->  ch )  <->  ( -.  ps 
<->  -.  ch ) )
21imbi2i 304 . . 3  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( ph  ->  ( -.  ps  <->  -.  ch )
) )
3 pm5.74 236 . . 3  |-  ( (
ph  ->  ( -.  ps  <->  -. 
ch ) )  <->  ( ( ph  ->  -.  ps )  <->  (
ph  ->  -.  ch )
) )
4 notbi 287 . . 3  |-  ( ( ( ph  ->  -.  ps )  <->  ( ph  ->  -. 
ch ) )  <->  ( -.  ( ph  ->  -.  ps )  <->  -.  ( ph  ->  -.  ch ) ) )
52, 3, 43bitri 263 . 2  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( -.  ( ph  ->  -.  ps )  <->  -.  ( ph  ->  -.  ch ) ) )
6 df-an 361 . . 3  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
7 df-an 361 . . 3  |-  ( (
ph  /\  ch )  <->  -.  ( ph  ->  -.  ch ) )
86, 7bibi12i 307 . 2  |-  ( ( ( ph  /\  ps ) 
<->  ( ph  /\  ch ) )  <->  ( -.  ( ph  ->  -.  ps )  <->  -.  ( ph  ->  -.  ch ) ) )
95, 8bitr4i 244 1  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( ( ph  /\ 
ps )  <->  ( ph  /\ 
ch ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  pm5.32i  619  pm5.32d  621  xordi  866  cbval2  2054  cbvex2  2055  rabbi  2846  rabxfrd  4703  asymref  5209  mpt22eqb  6138  dvdslelem  12849  cfilucfil4OLD  19226  cfilucfil4  19227  2sb5nd  28358  2sb5ndVD  28731  2sb5ndALT  28754  cbval2OLD7  29414  cbvex2OLD7  29415
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 178  df-an 361
  Copyright terms: Public domain W3C validator