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  2648  2eu6  2657  euind  3712  reuind  3741  sbnfc2  4419  opelopabt  5512  ssrel  5766  ssrelOLD  5767  ssrelrel  5780  fundif  6590  opabbrex  7463  fnoprabg  7535  tz7.48lem  8460  ssrelf  32600  bj-3exbi  36639  mpobi123f  38191  mptbi12f  38195  ismrc  42691  refimssco  43598  19.33-2  44373  pm11.63  44386  pm11.71  44388  axc5c4c711to11  44396  ichal  47447