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

Theorem 3jaob 1244
 Description: Disjunction of 3 antecedents. (Contributed by NM, 13-Sep-2011.)
Assertion
Ref Expression
3jaob (((φ χ θ) → ψ) ↔ ((φψ) (χψ) (θψ)))

Proof of Theorem 3jaob
StepHypRef Expression
1 3mix1 1124 . . . 4 (φ → (φ χ θ))
21imim1i 54 . . 3 (((φ χ θ) → ψ) → (φψ))
3 3mix2 1125 . . . 4 (χ → (φ χ θ))
43imim1i 54 . . 3 (((φ χ θ) → ψ) → (χψ))
5 3mix3 1126 . . . 4 (θ → (φ χ θ))
65imim1i 54 . . 3 (((φ χ θ) → ψ) → (θψ))
72, 4, 63jca 1132 . 2 (((φ χ θ) → ψ) → ((φψ) (χψ) (θψ)))
8 3jao 1243 . 2 (((φψ) (χψ) (θψ)) → ((φ χ θ) → ψ))
97, 8impbii 180 1 (((φ χ θ) → ψ) ↔ ((φψ) (χψ) (θψ)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∨ w3o 933   ∧ w3a 934 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  df-or 359  df-an 360  df-3or 935  df-3an 936 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator