Theorem ralimi 3140

Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)

Hypothesis

Ref	Expression
ralimi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ralimi	⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem ralimi

Step	Hyp	Ref	Expression
1		ralimi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	ralimia 3138	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2156  ∀wral 3096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894

This theorem depends on definitions:  df-bi 198  df-ral 3101

This theorem is referenced by:  2ralimi  3141  r19.26  3252  r19.29  3260  rr19.3v  3540  rr19.28v  3541  reu3  3594  uniiunlem  3889  reupick2  4114  uniss2  4664  ss2iun  4728  iineq2  4730  iunss2  4757  disjss2  4815  disjeq2  4816  reusv2lem5  5071  idrefOLD  5720  dmmptg  5846  wfisg  5928  fununi  6171  fnmptf  6223  fnmpt  6227  mpteqb  6516  chfnrn  6546  fvn0ssdmfun  6568  dffo5  6594  ffvresb  6612  fmptcof  6616  mpt22eqb  6995  ralrnmpt2  7001  abnexg  7190  tfis  7280  fun11uni  7346  fun11iun  7352  zfrep6  7360  mpt2exxg  7473  el2mpt2csbcl  7479  frxp  7517  smores  7681  riiner  8051  ixpn0  8173  boxriin  8183  unifi2  8491  wemaplem2  8687  rankonidlem  8934  acni3  9149  dfac5  9230  dfac12lem2  9247  kmlem6  9258  kmlem8  9260  kmlem13  9265  cfsmolem  9373  fin23lem40  9454  isf32lem2  9457  fin1a2s  9517  hsmexlem2  9530  hsmex3  9537  axcc4  9542  domtriomlem  9545  dcomex  9550  ac6num  9582  iundom  9645  unirnfdomd  9670  konigthlem  9671  iunctb  9677  gch3  9779  wununi  9809  wunpw  9810  wunpr  9812  eltsk2g  9854  tskpwss  9855  tskpw  9856  grupw  9898  gruurn  9901  intgru  9917  grothpw  9929  grothpwex  9930  grothomex  9932  axgroth3  9934  suplem1pr  10155  supexpr  10157  supsr  10214  fimaxre3  11251  xrsupexmnf  12349  xrinfmexpnf  12350  fsuppmapnn0fiublem  13009  fsuppmapnn0fiub  13010  fsuppmapnn0fiubex  13011  mptnn0fsuppd  13017  rexanre  14305  rexuz3  14307  cau3lem  14313  caubnd2  14316  caubnd  14317  rlim0  14458  rlim0lt  14459  climi2  14461  climi0  14462  climrlim2  14497  rlimres  14508  o1rlimmul  14568  caurcvg  14626  caurcvg2  14627  caucvg  14628  caucvgb  14629  sumeq2  14643  prodeq2  14861  ndvdssub  15348  gcdcllem1  15436  coprmproddvdslem  15590  vdwnnlem1  15912  imasaddfnlem  16389  catidex  16535  catlid  16544  catrid  16545  catcocl  16546  catpropd  16569  subcidcl  16704  funcid  16730  setcepi  16938  tsrss  17424  mgmidmo  17460  gsumval2  17481  isnmnd  17499  issubg2  17807  gagrpid  17924  gaass  17927  dprdcntz  18605  dprddisj  18606  abveq0  19026  abvmul  19029  abvtri  19030  psgndiflemB  20150  phllmhm  20183  ipcj  20185  ipeq0  20189  mdetmul  20637  pmatcollpw2lem  20792  eltg2b  20974  iincld  21054  iuncld  21060  isclo2  21103  neips  21128  neipeltop  21144  lmcvg  21277  t1t0  21363  hauscmplem  21420  bwth  21424  1stcelcls  21475  ptuni2  21590  pttopon  21610  ptcld  21627  ptcnplem  21635  txtube  21654  txlm  21662  xkococnlem  21673  fbun  21854  isfil2  21870  ptcmplem4  22069  ustssel  22219  isucn2  22293  ucncn  22299  metrest  22539  tngngp  22668  tngngp3  22670  ncvsi  23160  iscau4  23287  cmetcaulem  23296  caussi  23305  volfiniun  23527  iunmbl  23533  voliun  23534  mbfdm  23606  itg2seq  23722  itg2i1fseqle  23734  itg2i1fseq2  23736  iblcnlem  23768  limcresi  23862  limciun  23871  rolle  23966  ulmss  24364  rlimcnp  24905  colinearalg  26003  axpasch  26034  axeuclid  26056  axcontlem2  26058  axcontlem4  26060  axcontlem7  26063  axcontlem8  26064  fusgrregdegfi  26692  0grrgr  26703  rusgr1vtxlem  26710  wlkvtxeledg  26746  wlkdlem3  26808  wlkdlem4  26809  lfgriswlk  26812  lfgrwlknloop  26813  eulercrct  27414  1to3vfriendship  27455  frgrregorufr0  27498  isgrpo  27679  grpoidinv  27690  grpoideu  27691  grpoidval  27695  grpoidinv2  27697  vcidOLD  27746  vcdi  27747  vcdir  27748  vcass  27749  nvs  27845  nvz  27851  nvtri  27852  mdbr3  29483  mdbr4  29484  mdsl1i  29507  dmdbr6ati  29609  dmdbr7ati  29610  disjunsn  29731  hasheuni  30471  sigaclcu2  30507  prsiga  30518  measvunilem  30599  cntmeas  30613  omssubadd  30686  signsply0  30952  bnj1498  31450  cvmsdisj  31573  cvmshmeo  31574  cvmliftlem15  31601  cvmlift2lem12  31617  untangtr  31911  elpotr  32004  dfon2lem7  32012  dfon2lem8  32013  tfisg  32034  frpoinsg  32060  frinsg  32064  poseq  32072  opnrebl2  32635  fnemeet2  32681  fnejoin1  32682  fnejoin2  32683  dfgcd3  33485  ptrecube  33720  poimirlem25  33745  poimirlem26  33746  poimirlem27  33747  poimirlem30  33750  poimirlem31  33751  poimirlem32  33752  heicant  33755  ovoliunnfl  33762  voliunnfl  33764  volsupnfl  33765  frinfm  33840  caushft  33866  sstotbnd3  33884  prdstotbnd  33902  heibor1lem  33917  bfplem2  33931  opidonOLD  33960  exidu1  33964  grpomndo  33983  rngoideu  34011  rngodi  34012  rngodir  34013  rngoass  34014  rngoueqz  34048  idladdcl  34127  idllmulcl  34128  idlrmulcl  34129  mpt2bi123f  34279  iineq12f  34281  mptbi12f  34283  pmapglbx  35547  ltrnnid  35914  cdlemefrs32fva  36178  lerabdioph  37868  ltrabdioph  37871  nerabdioph  37872  dvdsrabdioph  37873  rencldnfi  37884  dford3  38093  pwelg  38362  pwinfi2  38364  ss2iundf  38448  neik0imk0p  38831  gneispace  38929  gneispace0nelrn  38935  ralbidar  39144  rexbidar  39145  uzubico2  40274  climuzlem  40452  xlimxrre  40534  bgoldbtbndlem2  42266  bgoldbtbndlem4  42268  mpt2exxg2  42681  iunord  42987