Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > ax2  Structured version GIF version 
Description: Axiom Frege. Axiom A2 of [Margaris] p. 49. This axiom "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 1691 ralim 2249 
Copyright terms: Public domain  W3C validator 