Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > a1iiOLD  Unicode version 
Description: Obsolete proof of a1ii 27 as of 21Jul2019. Shorter proof, but uses one more axiom. (Contributed by Wolf Lammen, 23Jul2013.) (New usage is discouraged.) (Proof modification is discouraged.) 
Ref  Expression 

a1iiOLD.1 
Ref  Expression 

a1iiOLD 
Step  Hyp  Ref  Expression 

1  a1iiOLD.1  . . 3  
2  1  a1i 11  . 2 
3  2  a1d 25  1 
Colors of variables: wff setvar class 
Syntax hints: > wi 4 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 
Copyright terms: Public domain  W3C validator 