Theorem ralimi 3099

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 3096	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-ral 3077

This theorem is used by:  rexbi  3118  ralrexbid  3119  r19.26  3122  r19.30  3129  2ralimi  3132  3ralimi  3133  4ralimi  3134  5ralimi  3135  6ralimi  3136  r19.21v  3187  rr19.3v  3620  rr19.28v  3621  reu3  3684  uniiunlem  4012  reupick2  4276  uniss2  4901  ss2iun  4969  iineq2  4971  dfiun2g  4987  iunss2  5007  disjss2  5072  disjeq2  5073  triin  5228  replem  5240  zfrep6  5241  reusv2lem5  5363  dmmptg  6243  frpoinsg  6346  fununi  6616  fnmptf  6676  fnmpt  6680  mpteqb  7014  chfnrn  7049  fvn0ssdmfun  7075  dffo5  7105  ffvresb  7127  fmptcof  7132  mpo2eqb  7553  ralrnmpo  7560  abnexg  7771  tfisg  7866  tfis  7867  fun11uni  7946  fiun  7956  f1iun  7957  zfrep6OLD  7968  mpoexxg  8089  el2mpocsbcl  8097  frxp  8141  xpord2indlem  8167  xpord3inddlem  8174  poseq  8178  smores  8364  naddcllem  8689  naddcom  8696  naddrid  8697  naddunif  8707  naddass  8710  riiner  8815  ixpn0  8962  boxriin  8972  unifi2  9338  wemaplem2  9545  frinsg  9759  rankonidlem  9842  acni3  10130  dfac5  10211  dfac12lem2  10227  kmlem6  10238  kmlem8  10240  kmlem13  10245  cfsmolem  10352  fin23lem40  10433  isf32lem2  10436  fin1a2s  10496  hsmexlem2  10509  hsmex3  10516  axcc4  10521  domtriomlem  10524  dcomex  10529  ac6num  10561  iundom  10630  unirnfdomd  10656  konigthlem  10657  iunctb  10663  gch3  10765  wununi  10795  wunpw  10796  wunpr  10798  eltsk2g  10840  tskpwss  10841  tskpw  10842  grupw  10884  gruurn  10887  intgru  10903  grothpw  10915  grothpwex  10916  grothomex  10918  axgroth3  10920  suplem1pr  11141  supexpr  11143  supsr  11201  fimaxre3  12267  xrsupexmnf  13439  xrinfmexpnf  13440  fsuppmapnn0fiublem  14137  fsuppmapnn0fiub  14138  fsuppmapnn0fiubex  14139  mptnn0fsuppd  14145  rexanre  15520  rexuz3  15522  cau3lem  15528  caubnd2  15531  caubnd  15532  rlim0  15681  rlim0lt  15682  climi2  15684  climi0  15685  climrlim2  15720  rlimres  15731  o1rlimmul  15792  caurcvg  15850  caurcvg2  15851  caucvg  15852  caucvgb  15853  sumeq2  15867  prodeq2  16087  ndvdssub  16585  gcdcllem1  16675  coprmproddvdslem  16843  vdwnnlem1  17179  imasaddfnlem  17706  catidex  17854  catlid  17863  catrid  17864  catcocl  17865  catpropd  17889  subcidcl  18025  funcid  18051  setcepi  18269  tsrss  18769  mgmidmo  18844  mgmidpfod  18863  gsumval2  18881  isnmnd  18933  issubg2  19358  gagrpid  19514  gaass  19517  cygabl  20111  dprdcntz  20230  dprddisj  20231  abveq0  21081  abvmul  21084  abvtri  21085  psgndiflemB  21912  phllmhm  21944  ipcj  21946  ipeq0  21950  mdetmul  22944  pmatcollpw2lem  23101  eltg2b  23283  iincld  23363  iuncld  23369  isclo2  23412  neips  23437  neipeltop  23453  lmcvg  23586  t1t0  23672  hauscmplem  23730  bwth  23734  1stcelcls  23786  ptuni2  23901  pttopon  23921  ptcld  23938  ptcnplem  23946  txtube  23965  txlm  23973  xkococnlem  23984  fbun  24165  isfil2  24181  ptcmplem4  24380  ustssel  24531  isucn2  24603  ucncn  24609  metrest  24849  tngngp  24979  tngngp3  24981  ncvsi  25478  iscau4  25606  cmetcaulem  25615  caussi  25624  volfiniun  25874  iunmbl  25880  voliun  25881  mbfdm  25953  itg2seq  26069  itg2i1fseqle  26081  itg2i1fseq2  26083  iblcnlem  26115  limcresi  26211  limciun  26220  rolle  26316  ulmss  26730  rlimcnp  27299  madebdayim  28280  addsuniflem  28393  oldfib  28769  colinearalg  29494  axpasch  29525  axeuclid  29547  axcontlem2  29549  axcontlem4  29551  axcontlem7  29554  axcontlem8  29555  lfuhgr2  29733  fusgrregdegfi  30156  0grrgr  30167  rusgr1vtxlem  30174  wlkvtxeledg  30210  wlkdlem3  30269  wlkdlem4  30270  lfgriswlk  30277  lfgrwlknloop  30278  eulercrct  30849  1to3vfriendship  30888  frgrregorufr0  30931  isgrpo  31105  grpoidinv  31116  grpoideu  31117  grpoidval  31121  grpoidinv2  31123  vcidOLD  31172  vcdi  31173  vcdir  31174  vcass  31175  nvs  31271  nvz  31277  nvtri  31278  mdbr3  32905  mdbr4  32906  mdsl1i  32929  dmdbr6ati  33031  dmdbr7ati  33032  disjunsn  33236  hasheuni  34764  sigaclcu2  34799  prsiga  34810  measvunilem  34892  cntmeas  34906  omssubadd  34979  signsply0  35227  bnj1498  35738  rmo6  35757  nummin  35775  axprALT2  35787  tz9.1regs  35859  onvf1odlem4  35954  srepdflem1  36005  srepdflem2  36006  cvmsdisj  36122  cvmshmeo  36123  cvmliftlem15  36150  cvmlift2lem12  36166  untangtr  36572  elpotr  36636  dfon2lem7  36644  dfon2lem8  36645  nmulprop  37032  opnrebl2  37202  fnemeet2  37248  fnejoin1  37249  fnejoin2  37250  weiunso  37347  weiunse  37349  weiunwe  37350  dfgcd3  38339  domalom  38421  ctbssinf  38423  nlpfvineqsn  38426  fvineqsnf1  38427  pibt1  38433  pibt2  38434  ptrecube  38632  poimirlem25  38657  poimirlem26  38658  poimirlem27  38659  poimirlem30  38662  poimirlem31  38663  poimirlem32  38664  heicant  38667  ovoliunnfl  38674  voliunnfl  38676  volsupnfl  38677  frinfm  38763  caushft  38789  sstotbnd3  38804  prdstotbnd  38822  heibor1lem  38837  bfplem2  38851  opidonOLD  38880  exidu1  38884  grpomndo  38903  rngoideu  38931  rngodi  38932  rngodir  38933  rngoass  38934  rngoueqz  38968  idladdcl  39047  idllmulcl  39048  idlrmulcl  39049  mpobi123f  39188  iineq12f  39190  mptbi12f  39192  dmqsblocks  39993  pmapglbx  40920  ltrnnid  41287  cdlemefrs32fva  41551  unitscyglem3  43341  fsuppind  43712  dffltz  43764  lerabdioph  43906  ltrabdioph  43909  nerabdioph  43910  dvdsrabdioph  43911  rencldnfi  43922  dford3  44129  pwelg  44655  pwinfi2  44657  ss2iundf  44753  neik0imk0p  45130  gneispace  45228  gneispace0nelrn  45234  ismnushort  45379  ralbidar  45522  rexbidar  45523  ssclaxsep  46066  uniclaxun  46070  uzubico2  46674  climuzlem  46847  xlimxrre  46935  2reuimp0  48278  bgoldbtbndlem2  48998  bgoldbtbndlem4  49000  mpoexxg2  49544  iuneqconst2  50028  iineqconst2  50029  iunord  50953