ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2rexbidv Structured version   GIF version

Theorem 2rexbidv 2343
Description: Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
Hypothesis
Ref Expression
2ralbidv.1 (φ → (ψχ))
Assertion
Ref Expression
2rexbidv (φ → (x A y B ψx A y B χ))
Distinct variable groups:   φ,x   φ,y
Allowed substitution hints:   ψ(x,y)   χ(x,y)   A(x,y)   B(x,y)

Proof of Theorem 2rexbidv
StepHypRef Expression
1 2ralbidv.1 . . 3 (φ → (ψχ))
21rexbidv 2321 . 2 (φ → (y B ψy B χ))
32rexbidv 2321 1 (φ → (x A y B ψx A y B χ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wrex 2301
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-rex 2306
This theorem is referenced by:  f1oiso  5408  elrnmpt2g  5555  elrnmpt2  5556  ralrnmpt2  5557  rexrnmpt2  5558  ovelrn  5591  eroveu  6133  genipv  6491  genpelxp  6493  genpelvl  6494  genpelvu  6495  genpelpw  6499  axcnre  6725  apreap  7331  apreim  7347
  Copyright terms: Public domain W3C validator