Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > ax2  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 238. (Contributed by NM, 5Aug1993.) 
Ref  Expression 

ax2  ⊢ ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))) 
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 set class 
This axiom is referenced by: a2i 10 id1 18 a2d 21 imdi 237 sbi1v 1630 
Copyright terms: Public domain  W3C validator 