Theorem alimi 1504

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

Hypothesis

Ref	Expression
alimi.1	⊢ (𝜑 → 𝜓)

Assertion

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

Proof of Theorem alimi

Step	Hyp	Ref	Expression
1		ax-5 1496	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
2		alimi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1500	1 ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1396

This theorem was proved from axioms:  ax-mp 5  ax-5 1496  ax-gen 1498

This theorem is referenced by:  2alimi  1505  al2imi  1507  alrimih  1518  hbal  1526  19.26  1530  19.33  1533  hbequid  1562  equidqe  1581  hbim  1594  hbor  1595  nford  1616  nfand  1617  nfal  1625  nfalt  1627  19.21ht  1630  exbi  1653  19.29  1669  19.25  1675  alexim  1694  alexnim  1697  19.9hd  1710  19.32r  1728  ax10  1765  spimh  1785  equvini  1806  nfexd  1809  stdpc4  1823  ax10oe  1845  sbcof2  1858  sb4bor  1883  nfsb2or  1885  spsbim  1891  ax16i  1906  sbi2v  1941  nfsbt  2029  nfsbd  2030  sbalyz  2052  hbsb4t  2066  dvelimor  2071  sbal2  2073  mo2n  2107  eumo0  2110  mor  2122  bm1.1  2216  alral  2578  rgen2a  2587  ralimi2  2593  rexim  2627  r19.32r  2680  ceqsalt  2830  spcgft  2884  spcegft  2886  spc2gv  2898  spc3gv  2900  rspct  2904  elabgt  2948  reu6  2996  sbciegft  3063  csbeq2  3152  csbnestgf  3181  ssrmof  3291  rabss2  3311  rabxmdc  3528  undif4  3559  ssdif0im  3561  inssdif0im  3564  ssundifim  3580  ralf0  3599  ralm  3600  intmin4  3961  dfiin2g  4008  invdisj  4086  trint  4207  a9evsep  4216  axnul  4219  csbexga  4222  exmidn0m  4297  exmidsssn  4298  exmidsssnc  4299  exmid0el  4300  ordunisuc2r  4618  tfi  4686  peano5  4702  ssrelrel  4832  issref  5126  iotanul  5309  iota4  5313  dffun5r  5345  fundif  5381  fv3  5671  mptfvex  5741  ssoprab2  6087  mpofvex  6379  tfri1dALT  6560  prodeq2w  12178  bj-nfalt  16462  elabgft1  16476  bj-rspgt  16484  bj-axemptylem  16588  bj-indind  16628  setindis  16663  bdsetindis  16665  bj-inf2vnlem1  16666  bj-inf2vn  16670  bj-inf2vn2  16671