Theorem 2alimi 1649

Description: Inference doubly quantifying both antecedent and consequent. (Contributed by NM, 3-Feb-2005.)

Hypothesis

Ref	Expression
alimi.1	|- ( ph -> ps )

Assertion

Ref	Expression
2alimi	|- ( A. x A. y ph -> A. x A. y ps )

Proof of Theorem 2alimi

Step	Hyp	Ref	Expression
1		alimi.1	. . 3 |- ( ph -> ps )
2	1	alimi 1648	. 2 |- ( A. y ph -> A. y ps )
3	2	alimi 1648	1 |- ( A. x A. y ph -> A. x A. y ps )

Syntax hints:   -> wi 4   A.wal 1397

This theorem was proved from axioms:  ax-mp 5  ax-gen 1633  ax-4 1646

This theorem is referenced by:  mo3OLD  2273  2mo  2318  2moOLD  2319  2eu6  2328  2eu6OLD  2329  euind  3228  reuind  3245  sbnfc2  3791  opelopabt  4690  ssrel  5021  ssrelrel  5033  opabbrex  6260  fnoprabg  6324  tz7.48lem  7046  ssrelf  27634  mpt2bi123f  30777  mptbi12f  30781  ismrc  30839  19.33-2  31495  pm11.63  31509  pm11.71  31511  axc5c4c711to11  31520  bj-3exbi  34593