MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.32 Structured version   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  cbval2OLD  1990  cbvex2  1991  rabbi  2878  rabxfrd  4736  asymref  5242  mpt22eqb  6171  dvdslelem  12886  cfilucfil4OLD  19265  cfilucfil4  19266  2sb5nd  28584  2sb5ndVD  28959  2sb5ndALT  28981  cbval2OLD7  29667  cbvex2OLD7  29668
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