Theorem alimi 1818

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Jan-1993.)

Hypothesis

Ref	Expression
alimi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
alimi	⊢ (∀𝑥𝜑 → ∀𝑥𝜓)

Proof of Theorem alimi

Step	Hyp	Ref	Expression
1		alim 1817	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
2		alimi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1804	1 ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1545

This theorem was proved from axioms:  ax-mp 5  ax-gen 1802  ax-4 1816

This theorem is referenced by:  2alimi  1819  ala1  1820  sylg  1830  19.38  1846  19.26  1877  19.33  1891  alcomimw  2050  hba1w  2056  hbalw  2058  exexw  2060  naev2  2070  2stdpc4  2081  spsbbi  2084  hbal  2178  nfim1  2211  axc4  2330  axc16i  2444  sb4a  2488  dfmoeu  2539  nexmo  2545  eu6  2578  darii  2669  cesare  2676  camestres  2677  festino  2678  baroco  2680  darapti  2688  calemes  2691  fesapo  2695  eqeq1d  2742  ralimi2  3072  rgen2a  3336  rmoeq1  3376  ceqsal1t  3465  spcgft  3497  vtoclgft  3500  rspct  3553  elabgt  3617  elabgtOLD  3618  reu6  3674  csbeq2  3843  ssrmof  3989  ralss  3994  rabss2OLD  4016  csbnestgfw  4357  csbnestgf  4362  undif4  4402  rzal  4429  falseral0OLD  4450  ralidmw  4451  ralidm  4452  intmin4  4914  dfiin2g  4967  invdisj  5065  disjss3  5078  axrep2  5209  replem  5217  zfrep6  5218  sepex  5229  ax6vsep  5232  axnul  5234  csbexg  5239  axpow3  5304  nfnid  5311  axprALT  5358  axprlem1  5359  axprlem4  5362  axprlem1OLD  5364  axprlem4OLD  5366  axprlem5OLD  5367  axprOLD  5368  axprg  5373  ssrelrel  5746  iresn0n0  6013  iotanul  6472  iota4  6473  fundif  6541  fv3  6852  zfrep6OLD  7904  ssfi  9104  elirrvOLD  9510  dfom3  9566  dfac5  10049  dfac2a  10050  dfac2b  10051  kmlem13  10083  zorng  10424  brdom3  10448  brdom4  10450  axpowndlem2  10519  axregnd  10525  axacndlem1  10528  axacndlem2  10529  axacndlem3  10530  axacndlem4  10531  axacnd  10533  ingru  10736  dfnn2  12185  trclfvcotr  14969  prodeq2w  15873  2ndcdisj2  23447  elons2  28275  dfn0s2  28349  pjnormssi  32264  disjin  32682  disjin2  32683  ssdifidlprm  33548  bnj1172  35190  bnj1174  35192  bnj1176  35194  bnj1523  35260  axprALT2  35297  r1omhfb  35300  fineqvpow  35303  r1omhfbregs  35325  axsepg2  35328  axsepg3  35329  axsepg3ALT  35330  axsepg4  35331  axpowg2  35335  axpowg3  35336  elpotr  36014  dfon2lem8  36023  distel  36036  hbimtg  36039  axtco1from2  36710  axtcond  36713  mh-setindnd  36772  bj-gl4  36913  bj-almpi  36937  bj-alanim  36945  bj-2albi  36946  bj-exim  36957  bj-aleximiALT  36959  bj-exalim  36962  bj-cbvaw  36988  bj-cbveaw  36990  bj-ssbid2ALT  37010  bj-sb  37037  bj-nfalt  37063  bj-nfext  37064  bj-nnfbd0  37098  bj-nnfalt  37140  bj-nnfext  37141  bj-cbv3tb  37147  bj-nfs1t2  37151  bj-hbaeb2  37178  bj-equsal1  37184  bj-equsal2  37185  2stdpc5  37189  bj-ceqsalt0  37244  bj-ceqsalt1  37245  bj-abv  37266  bj-bm1.3ii  37424  bj-axnul  37432  bj-rep  37433  exrecfnlem  37748  wl-dfcleq  37883  wl-moae  37894  wl-aleq  37913  wl-sb8ft  37928  wl-sb8eft  37929  wl-lem-nexmo  37945  wl-axc11rc11  37961  phpreu  37978  nninfnub  38125  mpobi123f  38536  eqab2  38624  trcoss  38946  hba1-o  39396  aecom-o  39400  ax12fromc15  39404  hbequid  39408  axc711  39413  axc711toc7  39415  axc711to11  39416  axc5c711  39417  axc5c711toc7  39419  axc5c711to11  39420  equidqe  39421  equid1ALT  39424  axc11nfromc11  39425  axc11n-16  39437  ax12eq  39440  ax12el  39441  ax12indi  39443  eu6w  43133  dfac11  43514  intimag  44107  intimasn  44108  frege70  44384  pm11.12  44826  2albi  44829  2exbi  44831  pm11.57  44840  pm11.61  44844  axc5c4c711toc7  44855  axc5c4c711to11  44856  axc11next  44857  pm13.192  44861  ralbidar  44895  rexbidar  44896  hbntal  45004  hbimpg  45005  hbexg  45007  ax6e2nd  45009  hbimpgVD  45354  ax6e2eqVD  45357  ax6e2ndVD  45358  ax6e2ndALT  45380  ssclaxsep  45433  quantgodelALT  47325  absnsb  47497  rexrsb  47570  ichal  47948  setrec1lem2  50185  setrec1lem4  50187