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  1656  equsalhw  1730  equsal  1900  sb6a  2055  ralbiia  2575  dfom2  4658  frinxp  4755  dfacacn  7767  kmlem8  7783  kmlem13  7788  kmlem14  7789  axgroth2  8447  uzindOLD  10106  filnetlem4  26330  sbidd-misc  28189  bnj1171  29030  bnj1253  29047  a12study10  29136  a12study10n  29137
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