Mathbox for Jeff Hankins 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > a1i24  Unicode version 
Description: Add two antecedents to a wff. (Contributed by Jeff Hankins, 5Aug2009.) 
Ref  Expression 

a1i24.1 
Ref  Expression 

a1i24 
Step  Hyp  Ref  Expression 

1  a1i24.1  . . 3  
2  1  a1dd 44  . 2 
3  2  a1d 23  1 
Colors of variables: wff set class 
Syntax hints: wi 4 
This theorem is referenced by: ad4ant13 27900 
This theorem was proved from axioms: ax1 5 ax2 6 axmp 8 
Copyright terms: Public domain  W3C validator 