Theorem 2alimi 1810

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-gen 1793  ax-4 1807

This theorem is referenced by:  alcomimw  2042  2mo  2651  2eu6  2660  euind  3746  reuind  3775  sbnfc2  4462  opelopabt  5551  ssrel  5806  ssrelOLD  5807  ssrelrel  5820  fundif  6627  opabbrex  7501  fnoprabg  7573  tz7.48lem  8497  ssrelf  32637  bj-3exbi  36582  mpobi123f  38122  mptbi12f  38126  ismrc  42657  refimssco  43569  19.33-2  44351  pm11.63  44364  pm11.71  44366  axc5c4c711to11  44374  ichal  47340