Theorem ralimi 3100

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3077

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

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

This theorem is used by:  rexbi  3119  ralrexbid  3120  r19.26  3123  r19.30  3130  2ralimi  3133  3ralimi  3134  4ralimi  3135  5ralimi  3136  6ralimi  3137  r19.21v  3188  rr19.3v  3621  rr19.28v  3622  reu3  3685  uniiunlem  4035  reupick2  4277  uniss2  4902  ss2iun  4970  iineq2  4972  dfiun2g  4988  iunss2  5008  disjss2  5073  disjeq2  5074  triin  5229  replem  5241  zfrep6  5242  reusv2lem5  5364  dmmptg  6242  frpoinsg  6345  fununi  6613  fnmptf  6673  fnmpt  6677  mpteqb  7011  chfnrn  7046  fvn0ssdmfun  7072  dffo5  7102  ffvresb  7124  fmptcof  7129  mpo2eqb  7550  ralrnmpo  7557  abnexg  7768  tfisg  7863  tfis  7864  fun11uni  7943  fiun  7953  f1iun  7954  zfrep6OLD  7965  mpoexxg  8086  el2mpocsbcl  8094  frxp  8136  xpord2indlem  8157  xpord3inddlem  8164  poseq  8168  smores  8353  naddcllem  8678  naddcom  8685  naddrid  8686  naddunif  8696  naddass  8699  riiner  8804  ixpn0  8951  boxriin  8961  unifi2  9327  wemaplem2  9534  frinsg  9748  rankonidlem  9831  acni3  10119  dfac5  10200  dfac12lem2  10216  kmlem6  10227  kmlem8  10229  kmlem13  10234  cfsmolem  10341  fin23lem40  10422  isf32lem2  10425  fin1a2s  10485  hsmexlem2  10498  hsmex3  10505  axcc4  10510  domtriomlem  10513  dcomex  10518  ac6num  10550  iundom  10619  unirnfdomd  10645  konigthlem  10646  iunctb  10652  gch3  10754  wununi  10784  wunpw  10785  wunpr  10787  eltsk2g  10829  tskpwss  10830  tskpw  10831  grupw  10873  gruurn  10876  intgru  10892  grothpw  10904  grothpwex  10905  grothomex  10907  axgroth3  10909  suplem1pr  11130  supexpr  11132  supsr  11190  fimaxre3  12256  xrsupexmnf  13428  xrinfmexpnf  13429  fsuppmapnn0fiublem  14126  fsuppmapnn0fiub  14127  fsuppmapnn0fiubex  14128  mptnn0fsuppd  14134  rexanre  15507  rexuz3  15509  cau3lem  15515  caubnd2  15518  caubnd  15519  rlim0  15668  rlim0lt  15669  climi2  15671  climi0  15672  climrlim2  15707  rlimres  15718  o1rlimmul  15779  caurcvg  15837  caurcvg2  15838  caucvg  15839  caucvgb  15840  sumeq2  15854  prodeq2  16074  ndvdssub  16572  gcdcllem1  16662  coprmproddvdslem  16830  vdwnnlem1  17166  imasaddfnlem  17693  catidex  17841  catlid  17850  catrid  17851  catcocl  17852  catpropd  17876  subcidcl  18012  funcid  18038  setcepi  18256  tsrss  18756  mgmidmo  18831  mgmidpfod  18850  gsumval2  18868  isnmnd  18920  issubg2  19345  gagrpid  19501  gaass  19504  cygabl  20098  dprdcntz  20217  dprddisj  20218  abveq0  21068  abvmul  21071  abvtri  21072  psgndiflemB  21899  phllmhm  21931  ipcj  21933  ipeq0  21937  mdetmul  22931  pmatcollpw2lem  23088  eltg2b  23270  iincld  23350  iuncld  23356  isclo2  23399  neips  23424  neipeltop  23440  lmcvg  23573  t1t0  23659  hauscmplem  23717  bwth  23721  1stcelcls  23773  ptuni2  23888  pttopon  23908  ptcld  23925  ptcnplem  23933  txtube  23952  txlm  23960  xkococnlem  23971  fbun  24152  isfil2  24168  ptcmplem4  24367  ustssel  24518  isucn2  24590  ucncn  24596  metrest  24836  tngngp  24966  tngngp3  24968  ncvsi  25465  iscau4  25593  cmetcaulem  25602  caussi  25611  volfiniun  25861  iunmbl  25867  voliun  25868  mbfdm  25940  itg2seq  26056  itg2i1fseqle  26068  itg2i1fseq2  26070  iblcnlem  26102  limcresi  26198  limciun  26207  rolle  26303  ulmss  26717  rlimcnp  27286  madebdayim  28267  addsuniflem  28380  oldfib  28756  colinearalg  29481  axpasch  29512  axeuclid  29534  axcontlem2  29536  axcontlem4  29538  axcontlem7  29541  axcontlem8  29542  lfuhgr2  29720  fusgrregdegfi  30143  0grrgr  30154  rusgr1vtxlem  30161  wlkvtxeledg  30197  wlkdlem3  30256  wlkdlem4  30257  lfgriswlk  30264  lfgrwlknloop  30265  eulercrct  30836  1to3vfriendship  30875  frgrregorufr0  30918  isgrpo  31092  grpoidinv  31103  grpoideu  31104  grpoidval  31108  grpoidinv2  31110  vcidOLD  31159  vcdi  31160  vcdir  31161  vcass  31162  nvs  31258  nvz  31264  nvtri  31265  mdbr3  32892  mdbr4  32893  mdsl1i  32916  dmdbr6ati  33018  dmdbr7ati  33019  disjunsn  33181  hasheuni  34710  sigaclcu2  34745  prsiga  34756  measvunilem  34838  cntmeas  34852  omssubadd  34925  signsply0  35173  bnj1498  35684  nummin  35711  axprALT2  35723  tz9.1regs  35785  onvf1odlem4  35868  cvmsdisj  36014  cvmshmeo  36015  cvmliftlem15  36042  cvmlift2lem12  36058  untangtr  36458  elpotr  36523  dfon2lem7  36531  dfon2lem8  36532  nmulprop  36919  opnrebl2  37089  fnemeet2  37135  fnejoin1  37136  fnejoin2  37137  weiunso  37234  weiunse  37236  weiunwe  37237  dfgcd3  38225  domalom  38307  ctbssinf  38309  nlpfvineqsn  38312  fvineqsnf1  38313  pibt1  38319  pibt2  38320  ptrecube  38518  poimirlem25  38543  poimirlem26  38544  poimirlem27  38545  poimirlem30  38548  poimirlem31  38549  poimirlem32  38550  heicant  38553  ovoliunnfl  38560  voliunnfl  38562  volsupnfl  38563  frinfm  38649  caushft  38675  sstotbnd3  38690  prdstotbnd  38708  heibor1lem  38723  bfplem2  38737  opidonOLD  38766  exidu1  38770  grpomndo  38789  rngoideu  38817  rngodi  38818  rngodir  38819  rngoass  38820  rngoueqz  38854  idladdcl  38933  idllmulcl  38934  idlrmulcl  38935  mpobi123f  39074  iineq12f  39076  mptbi12f  39078  dmqsblocks  39879  pmapglbx  40806  ltrnnid  41173  cdlemefrs32fva  41437  unitscyglem3  43227  fsuppind  43598  dffltz  43650  lerabdioph  43791  ltrabdioph  43794  nerabdioph  43795  dvdsrabdioph  43796  rencldnfi  43807  dford3  44014  pwelg  44545  pwinfi2  44547  ss2iundf  44644  neik0imk0p  45021  gneispace  45119  gneispace0nelrn  45125  ismnushort  45270  ralbidar  45413  rexbidar  45414  ssclaxsep  45950  uniclaxun  45954  uzubico2  46549  climuzlem  46722  xlimxrre  46810  2reuimp0  48153  bgoldbtbndlem2  48873  bgoldbtbndlem4  48875  mpoexxg2  49419  iuneqconst2  49902  iineqconst2  49903  iunord  50753