Theorem alimi 1455

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

Syntax hints:   → wi 4  ∀wal 1351

This theorem was proved from axioms:  ax-mp 5  ax-5 1447  ax-gen 1449

This theorem is referenced by:  2alimi  1456  al2imi  1458  alrimih  1469  hbal  1477  19.26  1481  19.33  1484  hbequid  1513  equidqe  1532  hbim  1545  hbor  1546  nford  1567  nfand  1568  nfal  1576  nfalt  1578  19.21ht  1581  exbi  1604  19.29  1620  19.25  1626  alexim  1645  alexnim  1648  19.9hd  1662  19.32r  1680  ax10  1717  spimh  1737  equvini  1758  nfexd  1761  stdpc4  1775  ax10oe  1797  sbcof2  1810  sb4bor  1835  nfsb2or  1837  spsbim  1843  ax16i  1858  sbi2v  1892  nfsbt  1976  nfsbd  1977  sbalyz  1999  hbsb4t  2013  dvelimor  2018  sbal2  2020  mo2n  2054  eumo0  2057  mor  2068  bm1.1  2162  alral  2522  rgen2a  2531  ralimi2  2537  rexim  2571  r19.32r  2623  ceqsalt  2763  spcgft  2814  spcegft  2816  spc2gv  2828  spc3gv  2830  rspct  2834  elabgt  2878  reu6  2926  sbciegft  2993  csbeq2  3081  csbnestgf  3109  ssrmof  3218  rabss2  3238  rabxmdc  3454  undif4  3485  ssdif0im  3487  inssdif0im  3490  ssundifim  3506  ralf0  3526  ralm  3527  intmin4  3872  dfiin2g  3919  invdisj  3997  trint  4116  a9evsep  4125  axnul  4128  csbexga  4131  exmidn0m  4201  exmidsssn  4202  exmidsssnc  4203  exmid0el  4204  ordunisuc2r  4513  tfi  4581  peano5  4597  ssrelrel  4726  issref  5011  iotanul  5193  iota4  5196  dffun5r  5228  fv3  5538  mptfvex  5601  ssoprab2  5930  mpofvex  6203  tfri1dALT  6351  prodeq2w  11559  bj-nfalt  14398  elabgft1  14412  bj-rspgt  14420  bj-axemptylem  14526  bj-indind  14566  setindis  14601  bdsetindis  14603  bj-inf2vnlem1  14604  bj-inf2vn  14608  bj-inf2vn2  14609