Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > pm2.86d  Unicode version 
Description: Deduction based on pm2.86 94. (Contributed by NM, 29Jun1995.) (Proof shortened by Wolf Lammen, 3Apr2013.) 
Ref  Expression 

pm2.86d.1 
Ref  Expression 

pm2.86d 
Step  Hyp  Ref  Expression 

1  ax1 5  . . 3  
2  pm2.86d.1  . . 3  
3  1, 2  syl5 28  . 2 
4  3  com23 72  1 
Colors of variables: wff set class 
Syntax hints: wi 4 
This theorem is referenced by: pm2.86 94 pm5.74 235 ax12olem6 1873 ax15 1961 a12study2 29134 
This theorem was proved from axioms: ax1 5 ax2 6 axmp 8 
Copyright terms: Public domain  W3C validator 