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  3246  rabss2  3266  rabxmdc  3482  undif4  3513  ssdif0im  3515  inssdif0im  3518  ssundifim  3534  ralf0  3553  ralm  3554  intmin4  3902  dfiin2g  3949  invdisj  4027  trint  4146  a9evsep  4155  axnul  4158  csbexga  4161  exmidn0m  4234  exmidsssn  4235  exmidsssnc  4236  exmid0el  4237  ordunisuc2r  4550  tfi  4618  peano5  4634  ssrelrel  4763  issref  5052  iotanul  5234  iota4  5238  dffun5r  5270  fv3  5581  mptfvex  5647  ssoprab2  5978  mpofvex  6263  tfri1dALT  6409  prodeq2w  11721  bj-nfalt  15410  elabgft1  15424  bj-rspgt  15432  bj-axemptylem  15538  bj-indind  15578  setindis  15613  bdsetindis  15615  bj-inf2vnlem1  15616  bj-inf2vn  15620  bj-inf2vn2  15621