Theorem alimi 1479

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

Syntax hints:   → wi 4  ∀wal 1371

This theorem was proved from axioms:  ax-mp 5  ax-5 1471  ax-gen 1473

This theorem is referenced by:  2alimi  1480  al2imi  1482  alrimih  1493  hbal  1501  19.26  1505  19.33  1508  hbequid  1537  equidqe  1556  hbim  1569  hbor  1570  nford  1591  nfand  1592  nfal  1600  nfalt  1602  19.21ht  1605  exbi  1628  19.29  1644  19.25  1650  alexim  1669  alexnim  1672  19.9hd  1686  19.32r  1704  ax10  1741  spimh  1761  equvini  1782  nfexd  1785  stdpc4  1799  ax10oe  1821  sbcof2  1834  sb4bor  1859  nfsb2or  1861  spsbim  1867  ax16i  1882  sbi2v  1917  nfsbt  2005  nfsbd  2006  sbalyz  2028  hbsb4t  2042  dvelimor  2047  sbal2  2049  mo2n  2083  eumo0  2086  mor  2097  bm1.1  2191  alral  2552  rgen2a  2561  ralimi2  2567  rexim  2601  r19.32r  2653  ceqsalt  2800  spcgft  2852  spcegft  2854  spc2gv  2866  spc3gv  2868  rspct  2872  elabgt  2916  reu6  2964  sbciegft  3031  csbeq2  3119  csbnestgf  3148  ssrmof  3258  rabss2  3278  rabxmdc  3494  undif4  3525  ssdif0im  3527  inssdif0im  3530  ssundifim  3546  ralf0  3565  ralm  3566  intmin4  3916  dfiin2g  3963  invdisj  4041  trint  4162  a9evsep  4171  axnul  4174  csbexga  4177  exmidn0m  4250  exmidsssn  4251  exmidsssnc  4252  exmid0el  4253  ordunisuc2r  4567  tfi  4635  peano5  4651  ssrelrel  4780  issref  5071  iotanul  5253  iota4  5257  dffun5r  5289  fundif  5324  fv3  5609  mptfvex  5675  ssoprab2  6011  mpofvex  6301  tfri1dALT  6447  prodeq2w  11917  bj-nfalt  15814  elabgft1  15828  bj-rspgt  15836  bj-axemptylem  15942  bj-indind  15982  setindis  16017  bdsetindis  16019  bj-inf2vnlem1  16020  bj-inf2vn  16024  bj-inf2vn2  16025