imp5g - Metamath Proof Explorer

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

Theorem imp5g 600

Description: An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)

**Hypothesis**
Ref	Expression
imp5.1

**Assertion**
Ref	Expression
imp5g

**Proof of Theorem imp5g**
Step	Hyp	Ref	Expression
1		imp5.1	. . 3
2	1	imp 429	. 2
3	2	imp4c 591	1

Colors of variables: wff setvar class

Syntax hints: ->wi 4 /\wa 369

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

This theorem depends on definitions: df-bi 185 df-an 371