impi - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > impi		Unicode version

Theorem impi 148

Description: An importation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 20-Jul-2013.)

**Hypothesis**
Ref	Expression
impi.1

**Assertion**
Ref	Expression
impi

**Proof of Theorem impi**
Step	Hyp	Ref	Expression
1		impi.1	. . 3
2	1	con3rr3 136	. 2
3	2	con1i 129	1

Colors of variables: wff setvar class

Syntax hints: -.wn 3 ->wi 4

This theorem is referenced by: simprim 150 dfbi1 192 imp 429

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8