Theorem alimi 1469

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

Syntax hints:   → wi 4  ∀wal 1362

This theorem was proved from axioms:  ax-mp 5  ax-5 1461  ax-gen 1463

This theorem is referenced by:  2alimi  1470  al2imi  1472  alrimih  1483  hbal  1491  19.26  1495  19.33  1498  hbequid  1527  equidqe  1546  hbim  1559  hbor  1560  nford  1581  nfand  1582  nfal  1590  nfalt  1592  19.21ht  1595  exbi  1618  19.29  1634  19.25  1640  alexim  1659  alexnim  1662  19.9hd  1676  19.32r  1694  ax10  1731  spimh  1751  equvini  1772  nfexd  1775  stdpc4  1789  ax10oe  1811  sbcof2  1824  sb4bor  1849  nfsb2or  1851  spsbim  1857  ax16i  1872  sbi2v  1907  nfsbt  1995  nfsbd  1996  sbalyz  2018  hbsb4t  2032  dvelimor  2037  sbal2  2039  mo2n  2073  eumo0  2076  mor  2087  bm1.1  2181  alral  2542  rgen2a  2551  ralimi2  2557  rexim  2591  r19.32r  2643  ceqsalt  2789  spcgft  2841  spcegft  2843  spc2gv  2855  spc3gv  2857  rspct  2861  elabgt  2905  reu6  2953  sbciegft  3020  csbeq2  3108  csbnestgf  3137  ssrmof  3247  rabss2  3267  rabxmdc  3483  undif4  3514  ssdif0im  3516  inssdif0im  3519  ssundifim  3535  ralf0  3554  ralm  3555  intmin4  3903  dfiin2g  3950  invdisj  4028  trint  4147  a9evsep  4156  axnul  4159  csbexga  4162  exmidn0m  4235  exmidsssn  4236  exmidsssnc  4237  exmid0el  4238  ordunisuc2r  4551  tfi  4619  peano5  4635  ssrelrel  4764  issref  5053  iotanul  5235  iota4  5239  dffun5r  5271  fv3  5584  mptfvex  5650  ssoprab2  5982  mpofvex  6272  tfri1dALT  6418  prodeq2w  11738  bj-nfalt  15494  elabgft1  15508  bj-rspgt  15516  bj-axemptylem  15622  bj-indind  15662  setindis  15697  bdsetindis  15699  bj-inf2vnlem1  15700  bj-inf2vn  15704  bj-inf2vn2  15705