Theorem 2alimi 1811

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

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-gen 1794  ax-4 1808

This theorem is referenced by:  alcomimw  2041  2mo  2647  2eu6  2656  euind  3729  reuind  3758  sbnfc2  4438  opelopabt  5536  ssrel  5791  ssrelOLD  5792  ssrelrel  5805  fundif  6614  opabbrex  7485  fnoprabg  7557  tz7.48lem  8482  ssrelf  32628  bj-3exbi  36618  mpobi123f  38170  mptbi12f  38174  ismrc  42717  refimssco  43625  19.33-2  44406  pm11.63  44419  pm11.71  44421  axc5c4c711to11  44429  ichal  47458