Theorem 2alimi 1606

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 1605	. 2 |- ( A. y ph -> A. y ps )
3	2	alimi 1605	1 |- ( A. x A. y ph -> A. x A. y ps )

Syntax hints:   -> wi 4   A.wal 1368

This theorem was proved from axioms:  ax-mp 5  ax-gen 1592  ax-4 1603

This theorem is referenced by:  mo3OLD  2305  moOLD  2311  2mo  2366  2moOLD  2367  2moOLDOLD  2368  2eu6  2377  2eu6OLD  2378  euind  3229  reuind  3246  sbnfc2  3790  opelopabt  4685  ssrel  5012  ssrelrel  5024  fnoprabg  6277  tz7.48lem  6982  ssrelf  26065  mpt2bi123f  29099  mptbi12f  29103  ismrc  29161  19.33-2  29758  pm11.63  29772  pm11.71  29774  axc5c4c711to11  29783  bj-3exbi  32430