Theorem alimi 1633

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

Hypothesis

Ref	Expression
alimi.1

Assertion

Ref	Expression
alimi

Proof of Theorem alimi

Step	Hyp	Ref	Expression
1		alim 1632	. 2
2		alimi.1	. 2
3	1, 2	mpg 1620	1

Syntax hints:  ->wi 4  A.wal 1393

This theorem is referenced by:  2alimi  1634  alrimih  1642  aleximiOLD  1659  ala1  1660  19.38  1662  19.26  1680  19.33  1695  alcomiw  1811  hba1w  1814  hbalw  1816  hbal  1844  axc4  1860  cbv3hv  1956  axc16i  2064  2stdpc4  2095  hba1-o  2228  aecom-o  2230  ax12  2234  hbequid  2239  axc711  2244  axc711toc7  2246  axc711to11  2247  axc5c711  2248  axc5c711toc7  2250  axc5c711to11  2251  equidqe  2252  equid1ALT  2255  axc11nfromc11  2256  axc11n-16  2268  ax12eq  2271  ax12el  2272  ax12indi  2274  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  eumo0OLD  2317  mo2OLD  2334  bm1.1OLD  2441  eqeq1d  2459  ralimi2  2847  rgen2a  2884  rgen2aOLD  2885  ceqsalt  3132  spcgft  3186  rspct  3203  elabgt  3243  reu6  3288  sbciegft  3358  csbeq2  3438  rabss2  3582  csbnestgf  3840  undif4  3883  ralf0  3936  intmin4  4316  dfiin2g  4363  invdisj  4441  trint  4560  axrep2  4565  ax6vsep  4577  axnul  4580  csbexg  4584  csbexgOLD  4586  nfnid  4681  axpr  4690  ssrelrel  5108  issref  5385  iotanul  5571  iota4  5574  fv3  5884  zfrep6  6768  dfom3  8085  dfac5  8530  dfac2a  8531  dfac2  8532  kmlem1  8551  kmlem13  8563  zorng  8905  brdom3  8927  brdom4  8929  axpowndlem2  8994  axpowndlem2OLD  8995  axregnd  9002  axacndlem1  9006  axacndlem2  9007  axacndlem3  9008  axacndlem4  9009  axacnd  9011  ingru  9214  dfnn2  10574  prodeq2w  13719  2ndcdisj2  19958  pjnormssi  27087  ssrmo  27393  disjin  27446  elpotr  29213  dfon2lem8  29222  distel  29236  hbimtg  29239  wl-aleq  29988  wl-lem-nexmo  30016  nninfnub  30244  mpt2bi123f  30571  mptbi12f  30575  dfac11  31008  pm11.12  31280  2albi  31283  2exbi  31285  pm11.57  31295  pm11.61  31299  axc5c4c711toc7  31311  axc5c4c711to11  31312  axc11next  31313  pm13.192  31317  ralbidar  31354  rexbidar  31355  rexrsb  32174  hbntal  33326  hbimpg  33327  hbexg  33329  ax6e2nd  33331  hbimpgVD  33704  ax6e2eqVD  33707  ax6e2ndVD  33708  ax6e2ndALT  33730  bnj956  33835  bnj1476  33905  bnj1533  33910  bnj1172  34057  bnj1174  34059  bnj1176  34061  bnj1523  34127  bj-gl4lem  34183  bj-alanim  34204  bj-2albi  34205  bj-2exbi  34206  bj-alrimhi  34213  bj-hbext  34264  bj-nfalt  34265  bj-nfext  34266  bj-cbv3tb  34271  bj-nfs1t2  34275  bj-stdpc4v  34334  bj-2stdpc4v  34335  bj-axrep2  34375  bj-hbaeb2  34391  bj-equsal1  34397  bj-equsal2  34398  2stdpc5  34402  bj-eumo0  34414  bj-ceqsalt0  34449  bj-ceqsalt1  34450  intimag  37770  intimasn  37771

This theorem was proved from axioms:  ax-mp 5  ax-gen 1618  ax-4 1631