Theorem alimi 1344

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

Syntax hints:   → wi 4  ∀wal 1241

This theorem was proved from axioms:  ax-mp 7  ax-5 1336  ax-gen 1338

This theorem is referenced by:  2alimi  1345  al2imi  1347  alrimih  1358  hbal  1366  19.26  1370  19.33  1373  hbequid  1406  equidqe  1425  hbim  1437  hbor  1438  nford  1459  nfand  1460  nfalt  1470  19.21ht  1473  exbi  1495  19.29  1511  19.25  1517  alexim  1536  alexnim  1539  19.9hd  1552  19.32r  1570  ax10  1605  spimh  1625  equvini  1641  nfexd  1644  stdpc4  1658  ax10oe  1678  sbcof2  1691  sb4bor  1716  nfsb2or  1718  spsbim  1724  ax16i  1738  sbi2v  1772  nfsbt  1850  nfsbd  1851  sbalyz  1875  hbsb4t  1889  dvelimor  1894  sbal2  1898  mo2n  1928  eumo0  1931  mor  1942  bm1.1  2025  alral  2367  rgen2a  2375  ralimi2  2381  rexim  2413  r19.32r  2457  ceqsalt  2580  spcgft  2630  spcegft  2632  spc2gv  2643  spc3gv  2645  rspct  2649  elabgt  2684  reu6  2730  sbciegft  2793  csbnestgf  2898  rabss2  3023  rabxmdc  3249  undif4  3284  ssdif0im  3286  inssdif0im  3291  ssundifim  3306  ralf0  3324  ralm  3325  intmin4  3643  dfiin2g  3690  invdisj  3759  trint  3869  a9evsep  3879  axnul  3882  csbexga  3885  ordunisuc2r  4240  tfi  4305  peano5  4321  ssrelrel  4440  issref  4707  iotanul  4882  iota4  4885  dffun5r  4914  fv3  5197  mptfvex  5256  ssoprab2  5561  mpt2fvex  5829  bj-nfalt  9904  elabgft1  9917  bj-rspgt  9925  bj-axemptylem  10012  bj-indind  10056  peano5setOLD  10065  setindis  10092  bdsetindis  10094  bj-inf2vnlem1  10095  bj-inf2vn  10099  bj-inf2vn2  10100