New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  pm5.32 GIF version

Theorem pm5.32 617
 Description: Distribution of implication over biconditional. Theorem *5.32 of [WhiteheadRussell] p. 125. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
pm5.32 ((φ → (ψχ)) ↔ ((φ ψ) ↔ (φ χ)))

Proof of Theorem pm5.32
StepHypRef Expression
1 notbi 286 . . . 4 ((ψχ) ↔ (¬ ψ ↔ ¬ χ))
21imbi2i 303 . . 3 ((φ → (ψχ)) ↔ (φ → (¬ ψ ↔ ¬ χ)))
3 pm5.74 235 . . 3 ((φ → (¬ ψ ↔ ¬ χ)) ↔ ((φ → ¬ ψ) ↔ (φ → ¬ χ)))
4 notbi 286 . . 3 (((φ → ¬ ψ) ↔ (φ → ¬ χ)) ↔ (¬ (φ → ¬ ψ) ↔ ¬ (φ → ¬ χ)))
52, 3, 43bitri 262 . 2 ((φ → (ψχ)) ↔ (¬ (φ → ¬ ψ) ↔ ¬ (φ → ¬ χ)))
6 df-an 360 . . 3 ((φ ψ) ↔ ¬ (φ → ¬ ψ))
7 df-an 360 . . 3 ((φ χ) ↔ ¬ (φ → ¬ χ))
86, 7bibi12i 306 . 2 (((φ ψ) ↔ (φ χ)) ↔ (¬ (φ → ¬ ψ) ↔ ¬ (φ → ¬ χ)))
95, 8bitr4i 243 1 ((φ → (ψχ)) ↔ ((φ ψ) ↔ (φ χ)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358 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  df-an 360 This theorem is referenced by:  pm5.32i  618  pm5.32d  620  xordi  865  cbval2  2004  cbvex2  2005  rabbi  2789
 Copyright terms: Public domain W3C validator