Mathbox for Alan Sare 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > biimpa21  Structured version Unicode version 
Description: biimpa 471 with commutation of the first and second conjuncts of the assertion. (Contributed by Alan Sare, 11Sep2016.) 
Ref  Expression 

biimpa21.1 
Ref  Expression 

biimpa21 
Step  Hyp  Ref  Expression 

1  biimpa21.1  . 2  
2  1  biimpac 473  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wb 177 wa 359 
This theorem is referenced by: 2sb5ndALT 29044 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 178 dfan 361 
Copyright terms: Public domain  W3C validator 