Theorem alimi 1455

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 1447	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
2		alimi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1451	1 ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1351

This theorem was proved from axioms:  ax-mp 5  ax-5 1447  ax-gen 1449

This theorem is referenced by:  2alimi  1456  al2imi  1458  alrimih  1469  hbal  1477  19.26  1481  19.33  1484  hbequid  1513  equidqe  1532  hbim  1545  hbor  1546  nford  1567  nfand  1568  nfal  1576  nfalt  1578  19.21ht  1581  exbi  1604  19.29  1620  19.25  1626  alexim  1645  alexnim  1648  19.9hd  1662  19.32r  1680  ax10  1717  spimh  1737  equvini  1758  nfexd  1761  stdpc4  1775  ax10oe  1797  sbcof2  1810  sb4bor  1835  nfsb2or  1837  spsbim  1843  ax16i  1858  sbi2v  1892  nfsbt  1976  nfsbd  1977  sbalyz  1999  hbsb4t  2013  dvelimor  2018  sbal2  2020  mo2n  2054  eumo0  2057  mor  2068  bm1.1  2162  alral  2522  rgen2a  2531  ralimi2  2537  rexim  2571  r19.32r  2623  ceqsalt  2765  spcgft  2816  spcegft  2818  spc2gv  2830  spc3gv  2832  rspct  2836  elabgt  2880  reu6  2928  sbciegft  2995  csbeq2  3083  csbnestgf  3111  ssrmof  3220  rabss2  3240  rabxmdc  3456  undif4  3487  ssdif0im  3489  inssdif0im  3492  ssundifim  3508  ralf0  3528  ralm  3529  intmin4  3874  dfiin2g  3921  invdisj  3999  trint  4118  a9evsep  4127  axnul  4130  csbexga  4133  exmidn0m  4203  exmidsssn  4204  exmidsssnc  4205  exmid0el  4206  ordunisuc2r  4515  tfi  4583  peano5  4599  ssrelrel  4728  issref  5013  iotanul  5195  iota4  5198  dffun5r  5230  fv3  5540  mptfvex  5603  ssoprab2  5933  mpofvex  6206  tfri1dALT  6354  prodeq2w  11566  bj-nfalt  14601  elabgft1  14615  bj-rspgt  14623  bj-axemptylem  14729  bj-indind  14769  setindis  14804  bdsetindis  14806  bj-inf2vnlem1  14807  bj-inf2vn  14811  bj-inf2vn2  14812