Mathbox for Jarvin Udandy 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > hirstLax3  Unicode version 
Description: The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of [Mendelson] p. 35. (Contributed by Jarvin Udandy, 7Feb2015.) (Proof modification is discouraged.) 
Ref  Expression 

hirstLax3 
Step  Hyp  Ref  Expression 

1  pm4.64 362  . 2  
2  pm4.66 410  . . 3  
3  pm2.64 765  . . . 4  
4  3  com12 29  . . 3 
5  2, 4  sylbi 188  . 2 
6  1, 5  syl5bi 209  1 
Colors of variables: wff set class 
Syntax hints: wn 3 wi 4 wo 358 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 178 dfor 360 
Copyright terms: Public domain  W3C validator 