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  1943  nfsbt  2032  nfsbd  2033  sbalyz  2055  hbsb4t  2069  dvelimor  2074  sbal2  2076  mo2n  2110  eumo0  2113  mor  2125  bm1.1  2219  alral  2589  rgen2a  2598  ralimi2  2604  rexim  2638  r19.32r  2691  ceqsalt  2842  spcgft  2896  spcegft  2898  spc2gv  2910  spc3gv  2912  rspct  2916  elabgt  2961  reu6  3009  sbciegft  3076  csbeq2  3165  csbnestgf  3194  ssrmof  3305  rabss2  3325  undif4  3575  ssdif0im  3577  inssdif0im  3580  ssundifim  3597  ralf0  3616  ralm  3617  intmin4  3982  dfiin2g  4029  invdisj  4107  trint  4228  a9evsep  4237  axnul  4240  csbexga  4243  exmidn0m  4319  exmidsssn  4320  exmidsssnc  4321  exmid0el  4322  ordunisuc2r  4641  tfi  4709  peano5  4725  ssrelrel  4855  issref  5150  iotanul  5333  iota4  5337  dffun5r  5369  fundif  5405  fv3  5698  mptfvex  5768  ssoprab2  6117  mpofvex  6414  tfri1dALT  6595  prodeq2w  12267  bj-nfalt  16648  elabgft1  16662  bj-rspgt  16670  bj-axemptylem  16774  bj-indind  16814  setindis  16849  bdsetindis  16851  bj-inf2vnlem1  16852  bj-inf2vn  16856  bj-inf2vn2  16857