Theorem alimi 1387

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

Syntax hints:   → wi 4  ∀wal 1285

This theorem was proved from axioms:  ax-mp 7  ax-5 1379  ax-gen 1381

This theorem is referenced by:  2alimi  1388  al2imi  1390  alrimih  1401  hbal  1409  19.26  1413  19.33  1416  hbequid  1449  equidqe  1468  hbim  1480  hbor  1481  nford  1502  nfand  1503  nfalt  1513  19.21ht  1516  exbi  1538  19.29  1554  19.25  1560  alexim  1579  alexnim  1582  19.9hd  1595  19.32r  1613  ax10  1649  spimh  1669  equvini  1685  nfexd  1688  stdpc4  1702  ax10oe  1722  sbcof2  1735  sb4bor  1760  nfsb2or  1762  spsbim  1768  ax16i  1783  sbi2v  1817  nfsbt  1895  nfsbd  1896  sbalyz  1920  hbsb4t  1934  dvelimor  1939  sbal2  1943  mo2n  1973  eumo0  1976  mor  1987  bm1.1  2070  alral  2417  rgen2a  2425  ralimi2  2431  rexim  2463  r19.32r  2510  ceqsalt  2639  spcgft  2689  spcegft  2691  spc2gv  2702  spc3gv  2704  rspct  2708  elabgt  2748  reu6  2795  sbciegft  2858  csbnestgf  2969  rabss2  3093  rabxmdc  3303  undif4  3333  ssdif0im  3335  inssdif0im  3338  ssundifim  3353  ralf0  3372  ralm  3373  intmin4  3701  dfiin2g  3748  invdisj  3817  trint  3928  a9evsep  3938  axnul  3941  csbexga  3944  exmid0el  4009  ordunisuc2r  4306  tfi  4372  peano5  4388  ssrelrel  4508  issref  4783  iotanul  4963  iota4  4966  dffun5r  4995  fv3  5293  mptfvex  5353  ssoprab2  5664  mpt2fvex  5932  tfri1dALT  6072  bj-nfalt  11153  elabgft1  11166  bj-rspgt  11174  bj-axemptylem  11271  bj-indind  11315  setindis  11350  bdsetindis  11352  bj-inf2vnlem1  11353  bj-inf2vn  11357  bj-inf2vn2  11358