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

Theorem ralrimiva 2386
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)
Hypothesis
Ref Expression
ralrimiva.1 ((φ x A) → ψ)
Assertion
Ref Expression
ralrimiva (φx A ψ)
Distinct variable group:   φ,x
Allowed substitution hints:   ψ(x)   A(x)

Proof of Theorem ralrimiva
StepHypRef Expression
1 ralrimiva.1 . . 3 ((φ x A) → ψ)
21ex 108 . 2 (φ → (x Aψ))
32ralrimiv 2385 1 (φx A ψ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wcel 1390  wral 2300
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-4 1397  ax-17 1416
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-ral 2305
This theorem is referenced by:  ralrimivvva  2396  rgen2  2399  rgen3  2400  nrexdv  2406  r19.29vva  2450  rabbidva  2542  ssrabdv  3013  ss2rabdv  3015  iuneq2dv  3669  disjeq2dv  3741  mpteq12dva  3829  triun  3858  issod  4047  peano2  4261  fun11iun  5090  fniinfv  5174  eqfnfv  5208  eqfnfvd  5211  dff3im  5255  dffo4  5258  foco2  5261  fmptd  5265  ffnfv  5266  fmpt2d  5270  ffvresb  5271  fconst2g  5319  fconstfvm  5322  resfunexg  5325  eufnfv  5332  fniunfv  5344  fcofo  5367  fliftel  5376  fliftfun  5379  fliftfuns  5381  riota5f  5435  grprinvlem  5637  grprinvd  5638  f1ocnvd  5644  suppssov1  5651  offval2  5668  ofrfval2  5669  offveqb  5672  caofref  5674  caofinvl  5675  opabex3d  5690  tfrlem1  5864  tfrlemisucaccv  5880  tfrlemiubacc  5885  omcl  5980  oeicl  5981  qliftfuns  6126  genprndl  6503  genprndu  6504  nqprloc  6527  ltexprlemrnd  6578  ltexprlemdisj  6579  recexprlemrnd  6600  recexprlemdisj  6601  negeu  6979  creur  7672  creui  7673  indstr2  8302  iooidg  8528  iccsupr  8585  icoshftf1o  8609  fznlem  8655  frecuzrdgfn  8859  iseqovex  8879  iseqval  8880  iseqfn  8881  iseq1  8882  iseqcl  8883  iseqp1  8884  iseqfveq2  8885  iseqfveq  8887
  Copyright terms: Public domain W3C validator