New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  2rexbiia GIF version

Theorem 2rexbiia 2648
 Description: Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
Hypothesis
Ref Expression
2rexbiia.1 ((x A y B) → (φψ))
Assertion
Ref Expression
2rexbiia (x A y B φx A y B ψ)
Distinct variable groups:   x,y   y,A
Allowed substitution hints:   φ(x,y)   ψ(x,y)   A(x)   B(x,y)

Proof of Theorem 2rexbiia
StepHypRef Expression
1 2rexbiia.1 . . 3 ((x A y B) → (φψ))
21rexbidva 2631 . 2 (x A → (y B φy B ψ))
32rexbiia 2647 1 (x A y B φx A y B ψ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   ∈ wcel 1710  ∃wrex 2615 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-rex 2620 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator