Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > ecase3d  Unicode version 
Description: Deduction for elimination by cases. (Contributed by NM, 2May1996.) (Proof shortened by Andrew Salmon, 7May2011.) 
Ref  Expression 

ecase3d.1  
ecase3d.2  
ecase3d.3 
Ref  Expression 

ecase3d 
Step  Hyp  Ref  Expression 

1  ecase3d.1  . . 3  
2  ecase3d.2  . . 3  
3  1, 2  jaod 370  . 2 
4  ecase3d.3  . 2  
5  3, 4  pm2.61d 152  1 
Colors of variables: wff set class 
Syntax hints: wn 3 wi 4 wo 358 
This theorem is referenced by: ecased 911 distrlem4pr 8838 atcvat4i 23750 cvrat4 29559 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 178 dfor 360 
Copyright terms: Public domain  W3C validator 