Theorem 2alimi 1844

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567

This proof depends on axioms:  ax-mp 5  ax-gen 1827  ax-4 1841

This theorem is used by:  alcomimw  2075  2mo  2673  2eu6  2681  euind  3681  reuind  3710  sbnfc2  4396  opelopabt  5505  ssrel  5758  ssrelrel  5771  fundif  6590  opabbrex  7474  fnoprabg  7544  tz7.48lemOLD  8455  ssrelf  33257  bj-3exbi  37595  mpobi123f  39188  mptbi12f  39192  ismrc  43806  refimssco  44701  19.33-2  45460  pm11.63  45473  pm11.71  45475  axc5c4c711to11  45483  ichal  48642