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

Theorem rexbidv 2305
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 1402 . 2 xφ
2 ralbidv.1 . 2 (φ → (ψχ))
31, 2rexbid 2303 1 (φ → (x A ψx A χ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wrex 2285
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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409
This theorem depends on definitions:  df-bi 110  df-nf 1330  df-rex 2290
This theorem is referenced by:  rexbii  2309  2rexbidv  2327  rexralbidv  2328  rexeqbi1dv  2492  rexeqbidv  2496  cbvrex2v  2520  rspc2ev  2641  rspc3ev  2643  ceqsrex2v  2653  sbcrext  2812  sbcrexg  2814  uniiunlem  3005  eliun  3635  dfiin2g  3664  dfiunv2  3667  nn0suc  4254  rexxpf  4410  elrnmpt  4510  elrnmptg  4513  elimag  4599  funcnvuni  4894  fun11iun  5072  fvelrnb  5146  fvelimab  5154  foelrn  5242  foco2  5243  elabrex  5322  abrexco  5323  f1oiso  5390  f1oiso2  5391  acexmidlemab  5430  acexmidlemcase  5431  grprinvlem  5618  abrexex2g  5670  abrexex2  5674  recseq  5843  frec0g  5902  frecsuclem3  5906  frecsuc  5907  nnaordex  6011  qseq2  6066  elqsg  6067  ltexnqq  6266  elinp  6328  prnmaxl  6342  prnminu  6343  prarloclem3  6351  ltdfpr  6360  genpdflem  6361  genipv  6363  genpassl  6379  genpassu  6380  ltexprlemm  6437  ltexprlemloc  6444  recexsrlem  6520  axprecex  6574  cnegex  6776  bj-inf2vnlem1  7188  bj-inf2vnlem2  7189  bj-nn0sucALT  7196
  Copyright terms: Public domain W3C validator