Theorem alimi 1448

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

Syntax hints:   → wi 4  ∀wal 1346

This theorem was proved from axioms:  ax-mp 5  ax-5 1440  ax-gen 1442

This theorem is referenced by:  2alimi  1449  al2imi  1451  alrimih  1462  hbal  1470  19.26  1474  19.33  1477  hbequid  1506  equidqe  1525  hbim  1538  hbor  1539  nford  1560  nfand  1561  nfal  1569  nfalt  1571  19.21ht  1574  exbi  1597  19.29  1613  19.25  1619  alexim  1638  alexnim  1641  19.9hd  1655  19.32r  1673  ax10  1710  spimh  1730  equvini  1751  nfexd  1754  stdpc4  1768  ax10oe  1790  sbcof2  1803  sb4bor  1828  nfsb2or  1830  spsbim  1836  ax16i  1851  sbi2v  1885  nfsbt  1969  nfsbd  1970  sbalyz  1992  hbsb4t  2006  dvelimor  2011  sbal2  2013  mo2n  2047  eumo0  2050  mor  2061  bm1.1  2155  alral  2515  rgen2a  2524  ralimi2  2530  rexim  2564  r19.32r  2616  ceqsalt  2756  spcgft  2807  spcegft  2809  spc2gv  2821  spc3gv  2823  rspct  2827  elabgt  2871  reu6  2919  sbciegft  2985  csbeq2  3073  csbnestgf  3101  ssrmof  3210  rabss2  3230  rabxmdc  3446  undif4  3477  ssdif0im  3479  inssdif0im  3482  ssundifim  3498  ralf0  3518  ralm  3519  intmin4  3859  dfiin2g  3906  invdisj  3983  trint  4102  a9evsep  4111  axnul  4114  csbexga  4117  exmidn0m  4187  exmidsssn  4188  exmidsssnc  4189  exmid0el  4190  ordunisuc2r  4498  tfi  4566  peano5  4582  ssrelrel  4711  issref  4993  iotanul  5175  iota4  5178  dffun5r  5210  fv3  5519  mptfvex  5581  ssoprab2  5909  mpofvex  6182  tfri1dALT  6330  prodeq2w  11519  bj-nfalt  13799  elabgft1  13813  bj-rspgt  13821  bj-axemptylem  13927  bj-indind  13967  setindis  14002  bdsetindis  14004  bj-inf2vnlem1  14005  bj-inf2vn  14009  bj-inf2vn2  14010