ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm5.74i Unicode version

Theorem pm5.74i 179
Description: Distribution of implication over biconditional (inference form). (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 178 . 2  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( ( ph  ->  ps )  <->  ( ph  ->  ch ) ) )
31, 2mpbi 144 1  |-  ( (
ph  ->  ps )  <->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  bitrd  187  imbi2i  225  bibi2d  231  ibib  244  ibibr  245  anclb  317  pm5.42  318  ancrb  320  equsalh  1689  equsal  1690  sb6a  1941  ralbiia  2426  dfdif3  3156  raaan  3439  exmid01  4091  isprm4  11727
  Copyright terms: Public domain W3C validator