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

Theorem ralrimiva 2435
 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 2434 1 (𝜑 → ∀𝑥𝐴 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 102   ∈ wcel 1434  ∀wral 2349 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 1377  ax-gen 1379  ax-4 1441  ax-17 1460 This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2354 This theorem is referenced by:  ralrimivvva  2445  rgen2  2448  rgen3  2449  nrexdv  2455  r19.29vva  2501  rabbidva  2593  ssrabdv  3074  ss2rabdv  3076  iuneq2dv  3707  disjeq2dv  3779  mpteq12dva  3867  triun  3896  issod  4082  frirrg  4113  frind  4115  peano2  4344  fun11iun  5178  fniinfv  5263  eqfnfv  5297  eqfnfvd  5300  dff3im  5344  dffo4  5347  foco2  5350  fmptd  5354  ffnfv  5355  fmpt2d  5359  ffvresb  5360  fconst2g  5408  fconstfvm  5411  resfunexg  5414  eufnfv  5421  fniunfv  5433  fcofo  5455  fliftel  5464  fliftfun  5467  fliftfuns  5469  riota5f  5523  grprinvlem  5726  grprinvd  5727  f1ocnvd  5733  suppssov1  5740  offval2  5757  ofrfval2  5758  offveqb  5761  caofref  5763  caofinvl  5764  opabex3d  5779  f1od2  5887  tfrlem1  5957  tfrlemisucaccv  5974  tfrlemiubacc  5979  tfr1onlemsucfn  5989  tfr1onlemsucaccv  5990  tfr1onlembxssdm  5992  tfr1onlembfn  5993  tfr1onlemubacc  5995  tfr1onlemaccex  5997  tfr1onlemres  5998  tfrcllemsucfn  6002  tfrcllemsucaccv  6003  tfrcllembxssdm  6005  tfrcllembfn  6006  tfrcllemubacc  6008  tfrcllemaccex  6010  tfrcllemres  6011  tfrcl  6013  rdgon  6035  freccllem  6051  frecfcllem  6053  omcl  6105  oeicl  6106  qliftfuns  6256  xpf1o  6385  eqsuptid  6469  eqinftid  6493  genprndl  6773  genprndu  6774  nqprloc  6797  ltexprlemrnd  6857  ltexprlemdisj  6858  lteupri  6869  recexprlemrnd  6881  recexprlemdisj  6882  caucvgprlemlim  6933  caucvgprprlemlim  6963  caucvgsrlembound  7032  caucvgsrlemgt1  7033  caucvgsrlemoffgt1  7037  caucvgsr  7040  elrealeu  7060  axcaucvglemcau  7126  axcaucvglemres  7127  negeu  7366  creur  8103  creui  8104  suprzclex  8526  supinfneg  8764  infsupneg  8765  indstr2  8777  iooidg  9008  iccsupr  9065  icoshftf1o  9089  fznlem  9136  exfzdc  9326  exbtwnzlemstep  9334  exbtwnzlemex  9336  frec2uzrdg  9491  frecuzrdgrcl  9492  frecuzrdgtcl  9494  frecuzrdgsuc  9496  frecuzrdgrclt  9497  frecuzrdgg  9498  frecuzrdgfunlem  9501  frecuzrdgsuctlem  9505  iseqovex  9529  iseqval  9530  iseqvalt  9532  iseq1  9533  iseq1t  9534  iseqfcl  9535  iseqfclt  9536  iseqcl  9537  iseqp1  9538  iseqp1t  9539  iseqoveq  9540  iseqfveq2  9544  iseqfveq  9546  iseqfeq  9547  iseqshft2  9548  monoord  9551  monoord2  9552  isermono  9553  iseqsplit  9554  iseqcaopr3  9556  iseqcaopr2  9557  iseqid3s  9562  iseqid  9563  iseqid2  9564  iseqhomo  9565  iseqz  9566  bccl  9791  sizeinfuni  9801  sizeennnuni  9803  shftf  9856  caucvgrelemcau  10004  cvg1nlemcau  10008  cvg1nlemres  10009  resqrexlemcvg  10043  resqrexlemglsq  10046  resqrexlemga  10047  maxabslemval  10232  negfi  10248  minmax  10250  climconst  10267  2clim  10278  climcn1  10285  climcn2  10286  cn1lem  10290  climsqz  10311  climsqz2  10312  climcau  10322  climrecvg1n  10323  serif0  10327  sumeq2d  10334  isumrblem  10337  fisumcvg  10338  dvdsssfz1  10397  zsupcllemstep  10485  infssuzex  10489  dvdsbnd  10492  bezoutlemstep  10530  bezoutlemmain  10531  bezoutlemle  10541  bezoutlemsup  10542  dfgcd3  10543  dfgcd2  10547  coprmgcdb  10614  isprm6  10670
 Copyright terms: Public domain W3C validator