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-1 5  ax-2 6  ax-3 7  ax-mp 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