Theorem 2alimi 1806

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

Syntax hints:   → wi 4  ∀wal 1531

This theorem was proved from axioms:  ax-mp 5  ax-gen 1789  ax-4 1803

This theorem is referenced by:  alcomiw  2038  2mo  2636  2eu6  2645  euind  3716  reuind  3745  sbnfc2  4438  opelopabt  5534  ssrel  5784  ssrelOLD  5785  ssrelrel  5798  fundif  6603  opabbrex  7471  fnoprabg  7543  tz7.48lem  8462  ssrelf  32484  bj-3exbi  36221  mpobi123f  37763  mptbi12f  37767  ismrc  42260  refimssco  43176  19.33-2  43958  pm11.63  43971  pm11.71  43973  axc5c4c711to11  43981  ichal  46940