Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > impi  Unicode version 
Description: An importation inference. (Contributed by NM, 5Aug1993.) (Proof shortened by Wolf Lammen, 20Jul2013.) 
Ref  Expression 

impi.1 
Ref  Expression 

impi 
Step  Hyp  Ref  Expression 

1  impi.1  . . 3  
2  1  con3rr3 130  . 2 
3  2  con1i 123  1 
Colors of variables: wff set class 
Syntax hints: wn 5 wi 6 
This theorem is referenced by: simprim 144 dfbi1 186 imp 420 
This theorem was proved from axioms: ax1 7 ax2 8 ax3 9 axmp 10 
Copyright terms: Public domain  W3C validator 