Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-2 GIF version

Axiom ax-2 6
 Description: Axiom Frege. Axiom A2 of [Margaris] p. 49. One of the 3 axioms of propositional calculus. It "distributes" an antecedent over two consequents. This axiom was part of Frege's original system and is known as Frege in the literature. It is also proved as Theorem *2.77 of [WhiteheadRussell] p. 108. The other direction of this axiom also turns out to be true, as demonstrated by pm5.41 238. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ax-2 ((φ → (ψχ)) → ((φψ) → (φχ)))

Detailed syntax breakdown of Axiom ax-2
StepHypRef Expression
1 wph . . 3 wff φ
2 wps . . . 4 wff ψ
3 wch . . . 4 wff χ
42, 3wi 4 . . 3 wff (ψχ)
51, 4wi 4 . 2 wff (φ → (ψχ))
61, 2wi 4 . . 3 wff (φψ)
71, 3wi 4 . . 3 wff (φχ)
86, 7wi 4 . 2 wff ((φψ) → (φχ))
95, 8wi 4 1 wff ((φ → (ψχ)) → ((φψ) → (φχ)))
 Colors of variables: wff set class This axiom is referenced by:  a2i  10  id1  18  a2d  21  imdi  237  sbi1v  1642
 Copyright terms: Public domain W3C validator