New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > ax-2 | GIF version |
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 353. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
ax-2 | ⊢ ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff φ | |
2 | wps | . . . 4 wff ψ | |
3 | wch | . . . 4 wff χ | |
4 | 2, 3 | wi 4 | . . 3 wff (ψ → χ) |
5 | 1, 4 | wi 4 | . 2 wff (φ → (ψ → χ)) |
6 | 1, 2 | wi 4 | . . 3 wff (φ → ψ) |
7 | 1, 3 | wi 4 | . . 3 wff (φ → χ) |
8 | 6, 7 | wi 4 | . 2 wff ((φ → ψ) → (φ → χ)) |
9 | 5, 8 | wi 4 | 1 wff ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))) |
Colors of variables: wff setvar class |
This axiom is referenced by: a2i 12 idALT 20 a2d 23 dfbi1gb 185 imdi 352 sbi1 2063 ralim 2686 difin0ss 3617 |
Copyright terms: Public domain | W3C validator |