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

Theorem pm5.74i 237
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 236 . 2  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( ( ph  ->  ps )  <->  ( ph  ->  ch ) ) )
31, 2mpbi 200 1  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  bitrd  245  imbi2i  304  bibi2d  310  ibib  332  ibibr  333  anclb  531  pm5.42  532  ancrb  534  cador  1400  cadan  1401  ax12b  1701  ax12bOLD  1702  equsalhw  1860  equsalhwOLD  1861  equsal  1999  equsalOLD  2000  sb6a  2193  ralbiia  2737  dfom2  4847  frinxp  4943  dfacacn  8021  kmlem8  8037  kmlem13  8042  kmlem14  8043  axgroth2  8700  uzindOLD  10364  filnetlem4  26410  bnj1171  29369  bnj1253  29386  equsalNEW7  29487  sb6aNEW7  29611
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 178
  Copyright terms: Public domain W3C validator