Theorem alimi 1443

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

Syntax hints:   → wi 4  ∀wal 1341

This theorem was proved from axioms:  ax-mp 5  ax-5 1435  ax-gen 1437

This theorem is referenced by:  2alimi  1444  al2imi  1446  alrimih  1457  hbal  1465  19.26  1469  19.33  1472  hbequid  1501  equidqe  1520  hbim  1533  hbor  1534  nford  1555  nfand  1556  nfal  1564  nfalt  1566  19.21ht  1569  exbi  1592  19.29  1608  19.25  1614  alexim  1633  alexnim  1636  19.9hd  1650  19.32r  1668  ax10  1705  spimh  1725  equvini  1746  nfexd  1749  stdpc4  1763  ax10oe  1785  sbcof2  1798  sb4bor  1823  nfsb2or  1825  spsbim  1831  ax16i  1846  sbi2v  1880  nfsbt  1964  nfsbd  1965  sbalyz  1987  hbsb4t  2001  dvelimor  2006  sbal2  2008  mo2n  2042  eumo0  2045  mor  2056  bm1.1  2150  alral  2511  rgen2a  2520  ralimi2  2526  rexim  2560  r19.32r  2612  ceqsalt  2752  spcgft  2803  spcegft  2805  spc2gv  2817  spc3gv  2819  rspct  2823  elabgt  2867  reu6  2915  sbciegft  2981  csbeq2  3069  csbnestgf  3097  ssrmof  3205  rabss2  3225  rabxmdc  3440  undif4  3471  ssdif0im  3473  inssdif0im  3476  ssundifim  3492  ralf0  3512  ralm  3513  intmin4  3852  dfiin2g  3899  invdisj  3976  trint  4095  a9evsep  4104  axnul  4107  csbexga  4110  exmidn0m  4180  exmidsssn  4181  exmidsssnc  4182  exmid0el  4183  ordunisuc2r  4491  tfi  4559  peano5  4575  ssrelrel  4704  issref  4986  iotanul  5168  iota4  5171  dffun5r  5200  fv3  5509  mptfvex  5571  ssoprab2  5898  mpofvex  6171  tfri1dALT  6319  prodeq2w  11497  bj-nfalt  13645  elabgft1  13659  bj-rspgt  13667  bj-axemptylem  13774  bj-indind  13814  setindis  13849  bdsetindis  13851  bj-inf2vnlem1  13852  bj-inf2vn  13856  bj-inf2vn2  13857