Theorem 2alimi 1814

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

Syntax hints:   → wi 4  ∀wal 1536

This theorem was proved from axioms:  ax-mp 5  ax-gen 1797  ax-4 1811

This theorem is referenced by:  alcomiw  2050  alcomiwOLD  2051  2mo  2710  2eu6  2719  euind  3663  reuind  3692  sbnfc2  4344  opelopabt  5384  ssrel  5621  ssrelrel  5633  fundif  6373  opabbrex  7186  fnoprabg  7254  tz7.48lem  8060  ssrelf  30379  bj-3exbi  34063  mpobi123f  35600  mptbi12f  35604  ismrc  39642  refimssco  40307  19.33-2  41086  pm11.63  41099  pm11.71  41101  axc5c4c711to11  41109  ichal  43983