reximia - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > reximia		Unicode version

Theorem reximia 2719

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.)

**Hypothesis**
Ref	Expression
reximia.1

**Assertion**
Ref	Expression
reximia

**Proof of Theorem reximia**
Step	Hyp	Ref	Expression
1		rexim 2718	. 2
2		reximia.1	. 2
3	1, 2	mprg 2683	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wcel 1710

wrex 2615

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

This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542 df-ral 2619 df-rex 2620

This theorem is referenced by: reximi 2721