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

Theorem pm5.32 617
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 286 . . . 4  |-  ( ( ps  <->  ch )  <->  ( -.  ps 
<->  -.  ch ) )
21imbi2i 303 . . 3  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( ph  ->  ( -.  ps  <->  -.  ch )
) )
3 pm5.74 235 . . 3  |-  ( (
ph  ->  ( -.  ps  <->  -. 
ch ) )  <->  ( ( ph  ->  -.  ps )  <->  (
ph  ->  -.  ch )
) )
4 notbi 286 . . 3  |-  ( ( ( ph  ->  -.  ps )  <->  ( ph  ->  -. 
ch ) )  <->  ( -.  ( ph  ->  -.  ps )  <->  -.  ( ph  ->  -.  ch ) ) )
52, 3, 43bitri 262 . 2  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( -.  ( ph  ->  -.  ps )  <->  -.  ( ph  ->  -.  ch ) ) )
6 df-an 360 . . 3  |-  ( (
ph  /\  ps )  <->  -.  ( ph  ->  -.  ps ) )
7 df-an 360 . . 3  |-  ( (
ph  /\  ch )  <->  -.  ( ph  ->  -.  ch ) )
86, 7bibi12i 306 . 2  |-  ( ( ( ph  /\  ps ) 
<->  ( ph  /\  ch ) )  <->  ( -.  ( ph  ->  -.  ps )  <->  -.  ( ph  ->  -.  ch ) ) )
95, 8bitr4i 243 1  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( ( ph  /\ 
ps )  <->  ( ph  /\ 
ch ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  pm5.32i  618  pm5.32d  620  xordi  865  cbval2  1957  cbvex2  1958  rabbi  2731  rabxfrd  4571  asymref  5075  mpt22eqb  5969  dvdslelem  12589  2sb5nd  28625  2sb5ndVD  29002  2sb5ndALT  29025  cbval2OLD7  29684  cbvex2OLD7  29685
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 177  df-an 360
  Copyright terms: Public domain W3C validator