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 1537

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

This theorem is referenced by:  alcomiw  2046  alcomiwOLD  2047  2mo  2650  2eu6  2658  euind  3659  reuind  3688  sbnfc2  4370  opelopabt  5445  ssrel  5693  ssrelOLD  5694  ssrelrel  5706  fundif  6483  opabbrex  7326  fnoprabg  7397  tz7.48lem  8272  ssrelf  30955  bj-3exbi  34798  mpobi123f  36320  mptbi12f  36324  ismrc  40523  refimssco  41215  19.33-2  42000  pm11.63  42013  pm11.71  42015  axc5c4c711to11  42023  ichal  44918