Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > pm2.61dda  Structured version Unicode version 
Description: Elimination of two antecedents. (Contributed by NM, 9Jul2013.) 
Ref  Expression 

pm2.61dda.1  
pm2.61dda.2  
pm2.61dda.3 
Ref  Expression 

pm2.61dda 
Step  Hyp  Ref  Expression 

1  pm2.61dda.3  . . . 4  
2  1  anassrs 646  . . 3 
3  pm2.61dda.2  . . . 4  
4  3  adantlr 713  . . 3 
5  2, 4  pm2.61dan 792  . 2 
6  pm2.61dda.1  . 2  
7  5, 6  pm2.61dan 792  1 
Colors of variables: wff setvar class 
Syntax hints: wn 3 wi 4 wa 367 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 ax3 8 
This theorem depends on definitions: dfbi 185 dfan 369 
This theorem is referenced by: lhpexle1lem 33004 lclkrlem2x 34530 
Copyright terms: Public domain  W3C validator 