Theorem pm2.61dane 2785

Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.)

Hypotheses

Ref	Expression
pm2.61dane.1	|- ( ( ph /\ A = B ) -> ps )
pm2.61dane.2	|- ( ( ph /\ A =/= B ) -> ps )

Assertion

Ref	Expression
pm2.61dane	|- ( ph -> ps )

Proof of Theorem pm2.61dane

Step	Hyp	Ref	Expression
1		pm2.61dane.1	. . 3 |- ( ( ph /\ A = B ) -> ps )
2	1	ex 434	. 2 |- ( ph -> ( A = B -> ps ) )
3		pm2.61dane.2	. . 3 |- ( ( ph /\ A =/= B ) -> ps )
4	3	ex 434	. 2 |- ( ph -> ( A =/= B -> ps ) )
5	2, 4	pm2.61dne 2784	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1379   =/= wne 2662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371  df-ne 2664

This theorem is referenced by:  pm2.61da2ne  2786  pm2.61da3ne  2787  pm2.61da3neOLD  2788  pm2.61iine  2789  disjxiun  4444  onfr  4917  f1oprswap  5855  soex  6727  riiner  7384  difsnen  7599  mapdom2  7688  nnunifi  7771  fofinf1o  7801  brwdom2  7999  cantnff  8093  cantnfp1  8100  cantnfp1OLD  8126  carddomi2  8351  wdomfil  8442  fin1a2lem10  8789  fin1a2lem11  8790  uzsupss  11174  xaddcom  11437  xnegdi  11440  xpncan  11443  xleadd1a  11445  xsubge0  11453  cnpart  13036  fsumcllem  13517  fsumrev2  13560  expcnv  13638  geomulcvg  13648  fsumdvds  13888  gcd0id  14020  nn0seqcvgd  14058  mulgcddvds  14104  pcge0  14244  pcneg  14256  pcdvdstr  14258  pcz  14263  pcprmpw2  14264  pcadd  14267  ramcl2  14393  0ramcl  14400  ramub1lem1  14403  ramcl  14406  mrerintcl  14852  mreriincl  14853  mreexexlem4d  14902  mreclatBAD  15674  psgnunilem1  16324  odmulg  16384  sylow1lem1  16424  pgpfi  16431  odadd1  16657  odadd2  16658  gsumval3OLD  16711  gsumval3  16714  gsumpt  16791  gsumptOLD  16792  dprdfcntz  16851  dprdfcntzOLD  16857  dprd2da  16893  ablfac1eulem  16925  pgpfaclem3  16936  abvneg  17283  lssssr  17399  lspsneq  17568  lspdisj2  17573  drngnidl  17676  cnsubrg  18274  riinopn  19212  riincld  19339  neipeltop  19424  hauscmplem  19700  cmpfi  19702  ptbasfi  19845  xkoccn  19883  txindislem  19897  txtube  19904  hmphindis  20061  fclscmp  20294  utop2nei  20516  nrginvrcn  20963  nmoleub  21001  blcvx  21066  xrsxmet  21077  xrsblre  21079  lebnumlem3  21226  cphsqrtcl2  21396  ovollb2  21663  ioorcl  21749  i1fmulc  21873  itg1mulc  21874  mbfi1fseqlem4  21888  dvlip  22157  dvne0  22175  ig1pdvds  22340  plyeq0lem  22370  plyeq0  22371  aannenlem2  22487  aalioulem6  22495  abelthlem8  22596  abelth  22598  cxpexp  22805  cxpge0  22820  cxpmul2  22826  abscxp2  22830  abscxpbnd  22883  cxpeq  22887  isosctrlem2  22909  atanrecl  22998  wilthlem2  23099  dchrabs2  23293  dchr1re  23294  lgsneg1  23351  lgsdirprm  23360  lgsdir  23361  lgsne0  23364  lgsdirnn0  23370  lgsdinn0  23371  2sqlem9  23404  rpvmasumlem  23428  dchrvmasumiflem1  23442  dchrisum0flblem1  23449  rpvmasum2  23453  pntrsumbnd2  23508  pntleml  23552  tgcolg  23697  tgidinside  23713  tgbtwnconn1lem2  23715  tgbtwnconn1lem3  23716  tglinethru  23758  tglnpt2  23762  tglineneq  23765  coltr  23768  coltr3  23770  colline  23771  mirreu3  23776  miriso  23791  colmid  23801  krippenlem  23803  midexlem  23805  ragflat  23817  ragcgr  23820  perprag  23833  perpdragALT  23834  colperpexlem1  23837  colperpexlem3  23839  mideu  23842  lmiisolem  23866  hypcgrlem1  23869  hypcgrlem2  23870  umgraex  24027  eupath2lem3  24683  nmcoplbi  26651  nmophmi  26654  nmbdfnlbi  26672  disjdifprg  27137  imadifxp  27159  xlt2addrd  27274  ssnnssfz  27293  nnlogbexp  27688  esumpr2  27742  mbfmcst  27898  probun  28026  0rrv  28058  sgncl  28145  signsvtn0  28195  fprodcllem  28688  btwnconn1lem11  29352  mblfinlem1  29656  mblfinlem2  29657  ismblfin  29660  itg2addnclem  29671  itgaddnclem2  29679  bddiblnc  29690  areacirclem4  29715  areacirc  29717  isbnd3  29911  blbnd  29914  rrnequiv  29962  jm2.19  30567  jm2.23  30570  lcmdvds  30842  nzss  30850  stoweidlem58  31386  ssnn0ssfz  32034  lsmsat  33823  lkrscss  33913  eqlkr  33914  lkrshpor  33922  atcvrj2b  34246  atltcvr  34249  3dim1  34281  3dim2  34282  3dim3  34283  ps-2  34292  2at0mat0  34339  dalemdnee  34480  dalem63  34549  lnatexN  34593  2llnma3r  34602  pmodlem1  34660  pmapjat1  34667  pclfinclN  34764  osumclN  34781  pexmidALTN  34792  lhpexle2lem  34823  lhpexle3lem  34825  4atexlemex6  34888  4atex  34890  trlnle  35000  trlval3  35001  cdlemc  35011  cdlemd9  35020  cdleme27N  35183  cdleme28c  35186  cdleme32fvaw  35253  cdleme42ke  35299  cdleme42keg  35300  cdleme42mgN  35302  cdleme17d  35312  cdleme48fvg  35314  cdleme50trn123  35368  cdlemb3  35420  cdlemg8  35445  cdlemg15a  35469  cdlemg15  35470  cdlemg16  35471  cdlemg16ALTN  35472  cdlemg16z  35473  cdlemg16zz  35474  cdlemg20  35499  cdlemg22  35501  cdlemg37  35503  cdlemg31d  35514  cdlemg39  35530  cdlemg40  35531  ltrncom  35552  tendotr  35644  cdlemk25-3  35718  cdlemk35s-id  35752  cdlemk39s-id  35754  cdlemk53b  35770  cdlemk53  35771  cdlemk55  35775  cdlemk35u  35778  cdlemk55u  35780  cdlemk39u  35782  cdlemk19u  35784  cdleml5N  35794  dia2dimlem7  35885  dia2dimlem13  35891  dih1dimatlem  36144  dihlsprn  36146  dihjat1lem  36243  dihjat1  36244  dvh2dim  36260  dochexmid  36283  lclkrlem1  36321  lclkrlem2i  36330  lclkrlem2t  36341  lcfrlem34  36391  lcfrlem38  36395  lcfrlem41  36398  mapdindp1  36535  mapdindp2  36536  mapdh6dN  36554  mapdh6jN  36560  mapdh8j  36603  mapdh8  36604  hdmap1l6d  36629  hdmap1l6j  36635  hdmap11lem2  36660  hdmap14lem7  36692