imp511 - Metamath Proof Explorer

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

Theorem imp511 602

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

**Hypothesis**
Ref	Expression
imp5.1

**Assertion**
Ref	Expression
imp511

**Proof of Theorem imp511**
Step	Hyp	Ref	Expression
1		imp5.1	. . 3
2	1	imp4a 589	. 2
3	2	imp44 596	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