Theorem 2alimi 1815

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

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-gen 1798  ax-4 1812

This theorem is referenced by:  alcomiw  2047  2mo  2645  2eu6  2653  euind  3721  reuind  3750  sbnfc2  4437  opelopabt  5533  ssrel  5783  ssrelOLD  5784  ssrelrel  5797  fundif  6598  opabbrex  7460  fnoprabg  7531  tz7.48lem  8441  ssrelf  31875  bj-3exbi  35542  mpobi123f  37078  mptbi12f  37082  ismrc  41487  refimssco  42406  19.33-2  43189  pm11.63  43202  pm11.71  43204  axc5c4c711to11  43212  ichal  46182