Mathbox for Jeff Hankins 
< Previous
Next >
Nearby theorems 

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

a1i13.1 
Ref  Expression 

a1i13 
Step  Hyp  Ref  Expression 

1  a1i13.1  . . 3  
2  1  a1d 22  . 2 
3  2  a1i 10  1 
Colors of variables: wff set class 
Syntax hints: wi 4 
This theorem is referenced by: comppfsc 25718 
This theorem was proved from axioms: ax1 5 ax2 6 axmp 8 
Copyright terms: Public domain  W3C validator 