Theorem 2alimi 1818

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 1817	. 2 ⊢ (∀𝑦𝜑 → ∀𝑦𝜓)
3	2	alimi 1817	1 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓)

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-gen 1801  ax-4 1815

This theorem is referenced by:  alcomiw  2049  alcomiwOLD  2050  2mo  2651  2eu6  2659  euind  3662  reuind  3691  sbnfc2  4375  opelopabt  5446  ssrel  5691  ssrelrel  5703  fundif  6479  opabbrex  7319  fnoprabg  7388  tz7.48lem  8256  ssrelf  30934  bj-3exbi  34777  mpobi123f  36299  mptbi12f  36303  ismrc  40503  refimssco  41168  19.33-2  41953  pm11.63  41966  pm11.71  41968  axc5c4c711to11  41976  ichal  44870