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

Theorem pm5.74i 245
Description: Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.)
Hypothesis
Ref Expression
pm5.74i.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
pm5.74i  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )

Proof of Theorem pm5.74i
StepHypRef Expression
1 pm5.74i.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 pm5.74 244 . 2  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( ( ph  ->  ps )  <->  ( ph  ->  ch ) ) )
31, 2mpbi 208 1  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  bitrd  253  imbi2i  312  bibi2d  318  ibib  342  ibibr  343  anclb  547  pm5.42  548  ancrb  550  cador  1433  cadanOLD  1435  ax13b  1745  equsalhw  1882  equsal  1995  sbcom3  2114  sb6aOLD  2164  2sb6rf  2168  ralbiia  2835  frinxp  5007  dfom2  6583  dfacacn  8416  kmlem8  8432  kmlem13  8437  kmlem14  8438  axgroth2  9098  uzindOLD  10842  wl-sbcom3  28554  filnetlem4  28745  bnj1171  32304  bnj1253  32321  bj-equsalv  32559
  Copyright terms: Public domain W3C validator