NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  pm5.74i GIF 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 (φ → (ψχ))
Assertion
Ref Expression
pm5.74i ((φψ) ↔ (φχ))

Proof of Theorem pm5.74i
StepHypRef Expression
1 pm5.74i.1 . 2 (φ → (ψχ))
2 pm5.74 235 . 2 ((φ → (ψχ)) ↔ ((φψ) ↔ (φχ)))
31, 2mpbi 199 1 ((φψ) ↔ (φχ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176
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 177
This theorem is referenced by:  bitrd  244  imbi2i  303  bibi2d  309  ibib  331  ibibr  332  anclb  530  pm5.42  531  ancrb  533  cador  1391  cadan  1392  ax12bOLD  1690  equsalhw  1838  equsalhwOLD  1839  equsal  1960  sb6a  2116  ralbiia  2646  clos1induct  5880
  Copyright terms: Public domain W3C validator