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 1537

This theorem was proved from axioms:  ax-mp 5  ax-gen 1795  ax-4 1809

This theorem is referenced by:  alcomiw  2044  2mo  2642  2eu6  2650  euind  3721  reuind  3750  sbnfc2  4437  opelopabt  5533  ssrel  5783  ssrelOLD  5784  ssrelrel  5797  fundif  6598  opabbrex  7464  fnoprabg  7535  tz7.48lem  8445  ssrelf  32109  bj-3exbi  35799  mpobi123f  37335  mptbi12f  37339  ismrc  41743  refimssco  42662  19.33-2  43445  pm11.63  43458  pm11.71  43460  axc5c4c711to11  43468  ichal  46434