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  1442  cadanOLD  1444  ax13b  1754  equsalhw  1892  equsal  2009  sbcom3  2128  sb6aOLD  2178  2sb6rf  2182  ralbiia  2894  frinxp  5064  dfom2  6680  dfacacn  8517  kmlem8  8533  kmlem13  8538  kmlem14  8539  axgroth2  9199  uzindOLD  10951  wl-sbcom3  29612  filnetlem4  29802  dirkertrigeqlem3  31400  fourierdlem26  31433  bnj1171  33135  bnj1253  33152  bj-equsalv  33392
  Copyright terms: Public domain W3C validator