Mathbox for Rodolfo Medina 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > jca2  Unicode version 
Description: Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 12Oct2010.) 
Ref  Expression 

jca2.1  
jca2.2 
Ref  Expression 

jca2 
Step  Hyp  Ref  Expression 

1  jca2.1  . 2  
2  jca2.2  . . 3  
3  2  a1i 10  . 2 
4  1, 3  jcad 519  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wa 358 
This theorem is referenced by: jca3 26813 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 177 dfan 360 
Copyright terms: Public domain  W3C validator 