Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

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

ax2 
Step  Hyp  Ref  Expression 

1  wph  . . 3  
2  wps  . . . 4  
3  wch  . . . 4  
4  2, 3  wi 4  . . 3 
5  1, 4  wi 4  . 2 
6  1, 2  wi 4  . . 3 
7  1, 3  wi 4  . . 3 
8  6, 7  wi 4  . 2 
9  5, 8  wi 4  1 
Colors of variables: wff set class 
This axiom is referenced by: a2i 11 id1 20 a2d 23 imdi 239 sbi1v 1749 ralim 2354 
Copyright terms: Public domain  W3C validator 