Mathbox for Alan Sare 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > ancomstVD  Structured version Unicode version 
Description: Closed form of ancoms 454. The following user's proof is completed by
invoking mmj2's unify command and using mmj2's StepSelector to pick all
remaining steps of the Metamath proof.

Ref  Expression 

ancomstVD 
Step  Hyp  Ref  Expression 

1  ancom 451  . 2  
2  imbi1 324  . 2  
3  1, 2  e0a 37132  1 
Colors of variables: wff setvar class 
Syntax hints: wi 4 wb 187 wa 370 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 ax3 8 
This theorem depends on definitions: dfbi 188 dfan 372 
This theorem is referenced by: (None) 
Copyright terms: Public domain  W3C validator 