Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > impt  Unicode version 
Description: Importation theorem expressed with primitive connectives. (Contributed by NM, 25Apr1994.) (Proof shortened by Wolf Lammen, 20Jul2013.) 
Ref  Expression 

impt 
Step  Hyp  Ref  Expression 

1  simprim 150  . 2  
2  simplim 151  . . 3  
3  2  imim1i 58  . 2 
4  1, 3  mpdi 42  1 
Colors of variables: wff setvar class 
Syntax hints: . wn 3 > wi 4 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 ax3 8 
Copyright terms: Public domain  W3C validator 