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

Theorem rexbidv 2321
Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
ralbidv.1 (φ → (ψχ))
Assertion
Ref Expression
rexbidv (φ → (x A ψx A χ))
Distinct variable group:   φ,x
Allowed substitution hints:   ψ(x)   χ(x)   A(x)

Proof of Theorem rexbidv
StepHypRef Expression
1 nfv 1418 . 2 xφ
2 ralbidv.1 . 2 (φ → (ψχ))
31, 2rexbid 2319 1 (φ → (x A ψx A χ))
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:  rexbii  2325  2rexbidv  2343  rexralbidv  2344  rexeqbi1dv  2508  rexeqbidv  2512  cbvrex2v  2536  rspc2ev  2658  rspc3ev  2660  ceqsrex2v  2670  sbcrext  2829  sbcrexg  2831  uniiunlem  3022  eliun  3652  dfiin2g  3681  dfiunv2  3684  nn0suc  4270  rexxpf  4426  elrnmpt  4526  elrnmptg  4529  elimag  4615  funcnvuni  4911  fun11iun  5090  fvelrnb  5164  fvelimab  5172  foelrn  5260  foco2  5261  elabrex  5340  abrexco  5341  f1oiso  5408  f1oiso2  5409  acexmidlemab  5449  acexmidlemcase  5450  grprinvlem  5637  abrexex2g  5689  abrexex2  5693  recseq  5862  tfr0  5878  freceq1  5919  frec0g  5922  frecsuclem3  5929  frecsuc  5930  nnaordex  6036  qseq2  6091  elqsg  6092  isfi  6177  enfi  6252  ltexnqq  6391  elinp  6456  prnmaxl  6470  prnminu  6471  prarloclem3  6479  ltdfpr  6488  genpdflem  6489  genipv  6491  genpassl  6507  genpassu  6508  ltexprlemm  6572  ltexprlemloc  6579  recexgt0sr  6661  archsr  6668  axprecex  6724  cnegex  6946  apreap  7331  recexap  7376  creur  7652  creui  7653  cju  7654  bj-inf2vnlem1  9354  bj-inf2vnlem2  9355  bj-nn0sucALT  9362
  Copyright terms: Public domain W3C validator