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

Theorem ralrimiva 2389
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)
Hypothesis
Ref Expression
ralrimiva.1 ((𝜑𝑥𝐴) → 𝜓)
Assertion
Ref Expression
ralrimiva (𝜑 → ∀𝑥𝐴 𝜓)
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimiva
StepHypRef Expression
1 ralrimiva.1 . . 3 ((𝜑𝑥𝐴) → 𝜓)
21ex 108 . 2 (𝜑 → (𝑥𝐴𝜓))
32ralrimiv 2388 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wcel 1393  wral 2303
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 1336  ax-gen 1338  ax-4 1400  ax-17 1419
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2308
This theorem is referenced by:  ralrimivvva  2399  rgen2  2402  rgen3  2403  nrexdv  2409  r19.29vva  2453  rabbidva  2545  ssrabdv  3016  ss2rabdv  3018  iuneq2dv  3675  disjeq2dv  3747  mpteq12dva  3835  triun  3864  issod  4053  frirrg  4084  peano2  4305  fun11iun  5134  fniinfv  5218  eqfnfv  5252  eqfnfvd  5255  dff3im  5299  dffo4  5302  foco2  5305  fmptd  5309  ffnfv  5310  fmpt2d  5314  ffvresb  5315  fconst2g  5363  fconstfvm  5366  resfunexg  5369  eufnfv  5376  fniunfv  5388  fcofo  5411  fliftel  5420  fliftfun  5423  fliftfuns  5425  riota5f  5479  grprinvlem  5682  grprinvd  5683  f1ocnvd  5689  suppssov1  5696  offval2  5713  ofrfval2  5714  offveqb  5717  caofref  5719  caofinvl  5720  opabex3d  5735  tfrlem1  5910  tfrlemisucaccv  5926  tfrlemiubacc  5931  omcl  6028  oeicl  6029  qliftfuns  6177  genprndl  6600  genprndu  6601  nqprloc  6624  ltexprlemrnd  6684  ltexprlemdisj  6685  lteupri  6696  recexprlemrnd  6708  recexprlemdisj  6709  caucvgprlemlim  6760  caucvgprprlemlim  6790  caucvgsrlembound  6859  caucvgsrlemgt1  6860  caucvgsrlemoffgt1  6864  caucvgsr  6867  elrealeu  6887  axcaucvglemcau  6953  axcaucvglemres  6954  negeu  7182  creur  7887  creui  7888  indstr2  8518  iooidg  8745  iccsupr  8802  icoshftf1o  8826  fznlem  8872  frecuzrdgfn  9076  iseqovex  9097  iseqval  9098  iseqfn  9099  iseq1  9100  iseqcl  9101  iseqf  9102  iseqp1  9103  iseqfveq2  9106  iseqfveq  9108  iseqfeq  9109  iseqshft2  9110  monoord  9113  monoord2  9114  isermono  9115  iseqsplit  9116  iseqcaopr3  9118  iseqcaopr2  9119  iseqid3s  9124  iseqid  9125  iseqhomo  9126  shftf  9309  caucvgrelemcau  9457  cvg1nlemcau  9461  cvg1nlemres  9462  resqrexlemcvg  9495  resqrexlemglsq  9498  resqrexlemga  9499  climconst  9688  2clim  9699  climcn1  9706  climcn2  9707  cn1lem  9711  climsqz  9732  climsqz2  9733  climcau  9743  climrecvg1n  9744  serif0  9748
  Copyright terms: Public domain W3C validator