Theorem 2alimi 1816

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

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-gen 1799  ax-4 1813

This theorem is referenced by:  alcomiw  2047  alcomiwOLD  2048  2mo  2650  2eu6  2658  euind  3654  reuind  3683  sbnfc2  4367  opelopabt  5438  ssrel  5683  ssrelrel  5695  fundif  6467  opabbrex  7306  fnoprabg  7375  tz7.48lem  8242  ssrelf  30856  bj-3exbi  34725  mpobi123f  36247  mptbi12f  36251  ismrc  40439  refimssco  41104  19.33-2  41889  pm11.63  41902  pm11.71  41904  axc5c4c711to11  41912  ichal  44806