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

Theorem ralrimiva 2442
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 113 . 2 (𝜑 → (𝑥𝐴𝜓))
32ralrimiv 2441 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1436  wral 2355
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-17 1462
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-ral 2360
This theorem is referenced by:  ralrimivvva  2452  rgen2  2455  rgen3  2456  nrexdv  2462  r19.29vva  2509  rabbidva  2603  ssrabdv  3089  ss2rabdv  3091  iuneq2dv  3734  disjeq2dv  3806  mpteq12dva  3894  triun  3924  issod  4120  frirrg  4151  frind  4153  peano2  4383  fun11iun  5237  fniinfv  5325  eqfnfv  5360  eqfnfvd  5363  dff3im  5407  dffo4  5410  fmptd  5415  ffnfv  5419  fmpt2d  5423  ffvresb  5424  fconst2g  5473  fconstfvm  5476  resfunexg  5479  eufnfv  5486  foco2  5494  fniunfv  5502  fcofo  5524  fliftel  5533  fliftfun  5536  fliftfuns  5538  riota5f  5593  grprinvlem  5796  grprinvd  5797  f1ocnvd  5803  suppssov1  5810  offval2  5827  ofrfval2  5828  offveqb  5831  caofref  5833  caofinvl  5834  opabex3d  5849  f1od2  5957  tfrlem1  6027  tfrlemisucaccv  6044  tfrlemiubacc  6049  tfr1onlemsucfn  6059  tfr1onlemsucaccv  6060  tfr1onlembxssdm  6062  tfr1onlembfn  6063  tfr1onlemubacc  6065  tfr1onlemaccex  6067  tfr1onlemres  6068  tfrcllemsucfn  6072  tfrcllemsucaccv  6073  tfrcllembxssdm  6075  tfrcllembfn  6076  tfrcllemubacc  6078  tfrcllemaccex  6080  tfrcllemres  6081  tfrcl  6083  rdgon  6105  freccllem  6121  frecfcllem  6123  omcl  6176  oeicl  6177  qliftfuns  6328  xpf1o  6512  mapxpen  6516  isinfinf  6565  fimax2gtrilemstep  6568  undifdcss  6585  eqsuptid  6636  eqinftid  6660  enomnilem  6738  nnnninf  6750  genprndl  7024  genprndu  7025  nqprloc  7048  ltexprlemrnd  7108  ltexprlemdisj  7109  lteupri  7120  recexprlemrnd  7132  recexprlemdisj  7133  caucvgprlemlim  7184  caucvgprprlemlim  7214  caucvgsrlembound  7283  caucvgsrlemgt1  7284  caucvgsrlemoffgt1  7288  caucvgsr  7291  elrealeu  7311  axcaucvglemcau  7377  axcaucvglemres  7378  negeu  7617  creur  8354  creui  8355  suprzclex  8777  supinfneg  9015  infsupneg  9016  indstr2  9028  iooidg  9259  iccsupr  9316  icoshftf1o  9340  fznlem  9387  exfzdc  9579  exbtwnzlemstep  9587  exbtwnzlemex  9589  frec2uzrdg  9744  frecuzrdgrcl  9745  frecuzrdgtcl  9747  frecuzrdgsuc  9749  frecuzrdgrclt  9750  frecuzrdgg  9751  frecuzrdgfunlem  9754  frecuzrdgsuctlem  9758  iseqovex  9787  iseqval  9788  iseqvalt  9790  iseq1  9791  iseq1t  9792  iseqfcl  9793  iseqfclt  9794  iseqcl  9795  iseqp1  9796  iseqp1t  9797  iseqoveq  9798  iseqfveq2  9802  iseqfveq  9804  iseqfeq  9805  iseqshft2  9806  monoord  9809  monoord2  9810  isermono  9811  iseqsplit  9812  iseqcaopr3  9814  iseqcaopr2  9815  iseqf1olemqk  9827  iseqf1olemjpcl  9828  iseqf1olemqpcl  9829  iseqf1olemfvp  9830  iseqf1olemqsumkj  9831  iseqf1olemqsumk  9832  iseqf1olemqsum  9833  iseqf1oleml  9836  iseqf1o  9837  iseqid3s  9841  iseqid  9842  iseqid2  9843  iseqhomo  9844  iseqz  9845  bccl  10071  hashinfuni  10081  hashennnuni  10083  shftf  10160  caucvgrelemcau  10308  cvg1nlemcau  10312  cvg1nlemres  10313  resqrexlemcvg  10347  resqrexlemglsq  10350  resqrexlemga  10351  maxabslemval  10536  negfi  10552  minmax  10554  climconst  10571  2clim  10582  climcn1  10589  climcn2  10590  cn1lem  10594  climsqz  10615  climsqz2  10616  climcau  10626  climrecvg1n  10627  serif0  10631  sumeq2dv  10647  isumrblem  10655  fisumcvg  10656  isummolem3  10659  isummolem2a  10660  zisum  10663  iisum  10664  fisum  10665  fsumf1o  10668  isumss  10669  fisumss  10670  dvdsssfz1  10728  zsupcllemstep  10816  infssuzex  10820  dvdsbnd  10823  bezoutlemstep  10861  bezoutlemmain  10862  bezoutlemle  10872  bezoutlemsup  10873  dfgcd3  10874  dfgcd2  10878  coprmgcdb  10945  isprm6  11001  phivalfi  11063  phibndlem  11067  dfphi2  11071  hashdvds  11072  phiprmpw  11073  phimullem  11076  hashgcdeq  11079  nnsf  11333  nninfalllemn  11336  nninfalllem1  11337  nninfall  11338  nninfself  11343  nninfsellemeq  11344  nninfsellemeqinf  11346  nninfsel  11347
  Copyright terms: Public domain W3C validator