Theorem 2alimi 1812

Description: Inference doubly quantifying both antecedent and consequent. (Contributed by NM, 3-Feb-2005.)

Hypothesis

Ref	Expression
alimi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
2alimi	⊢ (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓)

Proof of Theorem 2alimi

Step	Hyp	Ref	Expression
1		alimi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	alimi 1811	. 2 ⊢ (∀𝑦𝜑 → ∀𝑦𝜓)
3	2	alimi 1811	1 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓)

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-gen 1795  ax-4 1809

This theorem is referenced by:  alcomimw  2043  2mo  2641  2eu6  2650  euind  3695  reuind  3724  sbnfc2  4402  opelopabt  5492  ssrel  5745  ssrelOLD  5746  ssrelrel  5759  fundif  6565  opabbrex  7440  fnoprabg  7512  tz7.48lem  8409  ssrelf  32543  bj-3exbi  36604  mpobi123f  38156  mptbi12f  38160  ismrc  42689  refimssco  43596  19.33-2  44371  pm11.63  44384  pm11.71  44386  axc5c4c711to11  44394  ichal  47464