Mathbox for Mykola Mostovenko 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > Mathboxes > ax1hfs  Structured version GIF version 
Description: Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11Aug2018.) 
Ref  Expression 

ax1hfs  ⊢ (φ → (φ ∧ φ)) 
Step  Hyp  Ref  Expression 

1  axia3 101  . 2 ⊢ (φ → (φ → (φ ∧ φ)))  
2  1  pm2.43i 43  1 ⊢ (φ → (φ ∧ φ)) 
Colors of variables: wff set class 
Syntax hints: → wi 4 ∧ wa 97 
This theorem was proved from axioms: ax1 5 ax2 6 axmp 7 axia3 101 
This theorem is referenced by: (None) 
Copyright terms: Public domain  W3C validator 