Theorem 2alimi 1814

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

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-gen 1797  ax-4 1811

This theorem is referenced by:  alcomiw  2046  2mo  2643  2eu6  2651  euind  3685  reuind  3714  sbnfc2  4401  opelopabt  5494  ssrel  5743  ssrelOLD  5744  ssrelrel  5757  fundif  6555  opabbrex  7413  fnoprabg  7484  tz7.48lem  8392  ssrelf  31601  bj-3exbi  35157  mpobi123f  36694  mptbi12f  36698  ismrc  41082  refimssco  42001  19.33-2  42784  pm11.63  42797  pm11.71  42799  axc5c4c711to11  42807  ichal  45778