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  2017  cbvex2  2018  rabbi  2803  rabxfrd  4658  asymref  5162  mpt22eqb  6079  dvdslelem  12781  cfilucfil4  23927  2sb5nd  28061  2sb5ndVD  28438  2sb5ndALT  28461  cbval2OLD7  29121  cbvex2OLD7  29122
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