Mathbox for Alan Sare 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > imbi13  Structured version Unicode version 
Description: Join three logical equivalences to form equivalence of implications. imbi13 28678 is imbi13VD 29060 without virtual deductions and was automatically derived from imbi13VD 29060 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18Mar2012.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

imbi13 
Step  Hyp  Ref  Expression 

1  imbi12 28677  . 2  
2  imbi12 28677  . 2  
3  1, 2  syl9r 70  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wb 178 
This theorem is referenced by: trsbc 28699 trsbcVD 29063 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 ax3 8 
This theorem depends on definitions: dfbi 179 
Copyright terms: Public domain  W3C validator 