Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > bimsc1  Unicode version 
Description: Removal of conjunct from one side of an equivalence. (Contributed by NM, 5Aug1993.) 
Ref  Expression 

bimsc1 
Step  Hyp  Ref  Expression 

1  simpr 447  . . . 4  
2  ancr 532  . . . 4  
3  1, 2  impbid2 195  . . 3 
4  3  bibi2d 309  . 2 
5  4  biimpa 470  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wb 176 wa 358 
This theorem is referenced by: bm1.3ii 4160 
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 