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  2642  2eu6  2651  euind  3697  reuind  3726  sbnfc2  4404  opelopabt  5494  ssrel  5747  ssrelOLD  5748  ssrelrel  5761  fundif  6567  opabbrex  7442  fnoprabg  7514  tz7.48lem  8411  ssrelf  32549  bj-3exbi  36599  mpobi123f  38151  mptbi12f  38155  ismrc  42682  refimssco  43589  19.33-2  44364  pm11.63  44377  pm11.71  44379  axc5c4c711to11  44387  ichal  47457