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

Theorem pm5.74i 236
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 235 . 2  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( ( ph  ->  ps )  <->  ( ph  ->  ch ) ) )
31, 2mpbi 199 1  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  bitrd  244  imbi2i  303  bibi2d  309  ibib  331  ibibr  332  anclb  530  pm5.42  531  ancrb  533  cador  1381  cadan  1382  ax12bOLD  1675  equsalhw  1742  equsal  1913  sb6a  2068  ralbiia  2588  dfom2  4674  frinxp  4771  dfacacn  7783  kmlem8  7799  kmlem13  7804  kmlem14  7805  axgroth2  8463  uzindOLD  10122  filnetlem4  26433  sbidd-misc  28443  bnj1171  29346  bnj1253  29363  equsalNEW7  29464  sb6aNEW7  29583  a12study10  29758  a12study10n  29759
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
  Copyright terms: Public domain W3C validator