Theorem alimi 1739

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Jan-1993.)

Hypothesis

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

Assertion

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

Proof of Theorem alimi

Step	Hyp	Ref	Expression
1		alim 1738	. 2 |- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
2		alimi.1	. 2 |- ( ph -> ps )
3	1, 2	mpg 1724	1 |- ( A. x ph -> A. x ps )

Syntax hints:   -> wi 4   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-gen 1722  ax-4 1737

This theorem is referenced by:  2alimi  1740  ala1  1741  sylg  1750  19.38  1766  nfntOLDOLD  1783  19.26  1798  19.33  1812  nfimdOLDOLD  1824  alcomiw  1971  hba1w  1974  hba1wOLD  1975  hbalw  1977  hbal  2036  nfim1  2067  axc4  2130  axc16i  2322  ax12OLD  2341  2stdpc4  2354  mo2v  2477  eqeq1d  2624  ralimi2  2949  rgen2a  2977  ceqsalt  3228  spcgft  3285  rspct  3302  elabgt  3347  reu6  3395  sbciegft  3466  csbeq2  3537  rabss2  3685  csbnestgf  3996  undif4  4035  ralf0OLD  4079  falseral0  4081  intmin4  4506  dfiin2g  4553  invdisj  4638  disjss3  4652  axrep2  4773  ax6vsep  4785  axnul  4788  csbexg  4792  nfnid  4897  axpr  4905  ssrelrel  5220  issref  5509  iotanul  5866  iota4  5869  fundif  5935  fv3  6206  zfrep6  7134  dfom3  8544  dfac5  8951  dfac2a  8952  dfac2  8953  kmlem13  8984  zorng  9326  brdom3  9350  brdom4  9352  axpowndlem2  9420  axregnd  9426  axacndlem1  9429  axacndlem2  9430  axacndlem3  9431  axacndlem4  9432  axacnd  9434  ingru  9637  dfnn2  11033  trclfvcotr  13750  prodeq2w  14642  2ndcdisj2  21260  pjnormssi  29027  ssrmo  29334  disjin  29399  disjin2  29400  bnj1172  31069  bnj1174  31071  bnj1176  31073  bnj1523  31139  elpotr  31686  dfon2lem8  31695  distel  31709  hbimtg  31712  bj-gl4lem  32579  bj-alanim  32596  bj-2albi  32597  bj-2exbi  32599  bj-alrimhi  32604  bj-exalim  32611  bj-ssbbi  32622  bj-ssb1a  32632  bj-ssbequ2  32643  bj-ssbid2ALT  32646  bj-sb  32677  bj-hbext  32701  bj-nfalt  32702  bj-nfext  32703  bj-cbv3tb  32711  bj-nfs1t2  32715  bj-stdpc4v  32754  bj-2stdpc4v  32755  bj-axrep2  32789  bj-hbaeb2  32805  bj-equsal1  32811  bj-equsal2  32812  2stdpc5  32816  bj-eumo0  32830  bj-ceqsalt0  32873  bj-ceqsalt1  32874  wl-hbnaev  33305  wl-aleq  33322  wl-lem-nexmo  33349  phpreu  33393  nninfnub  33547  mpt2bi123f  33971  mptbi12f  33975  hba1-o  34182  aecom-o  34186  ax12fromc15  34190  hbequid  34194  axc711  34199  axc711toc7  34201  axc711to11  34202  axc5c711  34203  axc5c711toc7  34205  axc5c711to11  34206  equidqe  34207  equid1ALT  34210  axc11nfromc11  34211  axc11n-16  34223  ax12eq  34226  ax12el  34227  ax12indi  34229  dfac11  37632  intimag  37948  intimasn  37949  frege70  38227  pm11.12  38574  2albi  38577  2exbi  38579  pm11.57  38589  pm11.61  38593  axc5c4c711toc7  38605  axc5c4c711to11  38606  axc11next  38607  pm13.192  38611  ralbidar  38649  rexbidar  38650  hbntal  38769  hbimpg  38770  hbexg  38772  ax6e2nd  38774  hbimpgVD  39140  ax6e2eqVD  39143  ax6e2ndVD  39144  ax6e2ndALT  39166  rexrsb  41169  setrec1lem2  42435  setrec1lem4  42437