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

Theorem pm5.74i 248
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 247 . 2  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( ( ph  ->  ps )  <->  ( ph  ->  ch ) ) )
31, 2mpbi 211 1  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  bitrd  256  imbi2i  313  bibi2d  319  ibib  343  ibibr  344  anclb  549  pm5.42  550  ancrb  552  cador  1506  ax13b  1857  equsalhw  2003  equsal  2091  sbcom3  2206  2sb6rf  2248  ralbiia  2862  frinxp  4920  dfom2  6708  dfacacn  8569  kmlem8  8585  kmlem13  8590  kmlem14  8591  axgroth2  9249  bnj1171  29597  bnj1253  29614  filnetlem4  30822  bj-equsalv  31089  bj-equsalvv  31090  wl-sbcom3  31629  elintima  35884
  Copyright terms: Public domain W3C validator