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  1786  equvini  1807  nfexd  1810  stdpc4  1824  ax10oe  1846  sbcof2  1859  sb4bor  1884  nfsb2or  1886  spsbim  1892  ax16i  1907  sbi2v  1942  nfsbt  2030  nfsbd  2031  sbalyz  2053  hbsb4t  2067  dvelimor  2072  sbal2  2074  mo2n  2108  eumo0  2111  mor  2123  bm1.1  2217  alral  2587  rgen2a  2596  ralimi2  2602  rexim  2636  r19.32r  2689  ceqsalt  2839  spcgft  2893  spcegft  2895  spc2gv  2907  spc3gv  2909  rspct  2913  elabgt  2957  reu6  3005  sbciegft  3072  csbeq2  3161  csbnestgf  3190  ssrmof  3300  rabss2  3320  rabxmdc  3539  undif4  3570  ssdif0im  3572  inssdif0im  3575  ssundifim  3592  ralf0  3611  ralm  3612  intmin4  3976  dfiin2g  4023  invdisj  4101  trint  4222  a9evsep  4231  axnul  4234  csbexga  4237  exmidn0m  4313  exmidsssn  4314  exmidsssnc  4315  exmid0el  4316  ordunisuc2r  4635  tfi  4703  peano5  4719  ssrelrel  4849  issref  5144  iotanul  5327  iota4  5331  dffun5r  5363  fundif  5399  fv3  5692  mptfvex  5762  ssoprab2  6108  mpofvex  6400  tfri1dALT  6581  prodeq2w  12238  bj-nfalt  16528  elabgft1  16542  bj-rspgt  16550  bj-axemptylem  16654  bj-indind  16694  setindis  16729  bdsetindis  16731  bj-inf2vnlem1  16732  bj-inf2vn  16736  bj-inf2vn2  16737