Theorem pm2.61dane 2700

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 432	. 2 |- ( ph -> ( A = B -> ps ) )
3		pm2.61dane.2	. . 3 |- ( ( ph /\ A =/= B ) -> ps )
4	3	ex 432	. 2 |- ( ph -> ( A =/= B -> ps ) )
5	2, 4	pm2.61dne 2699	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1399   =/= wne 2577

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 369  df-ne 2579

This theorem is referenced by:  pm2.61da2ne  2701  pm2.61da3ne  2702  pm2.61da3neOLD  2703  pm2.61iine  2704  disjxiun  4364  onfr  4831  f1oprswap  5763  soex  6642  riiner  7302  difsnen  7518  mapdom2  7607  nnunifi  7686  fofinf1o  7716  brwdom2  7914  cantnff  8006  cantnfp1  8013  cantnfp1OLD  8039  carddomi2  8264  wdomfil  8355  fin1a2lem10  8702  fin1a2lem11  8703  uzsupss  11093  xaddcom  11358  xnegdi  11361  xpncan  11364  xleadd1a  11366  xsubge0  11374  cnpart  13075  fsumcllem  13556  fsumrev2  13599  expcnv  13677  geomulcvg  13687  fprodcllem  13760  fsumdvds  14031  gcd0id  14163  nn0seqcvgd  14201  mulgcddvds  14247  pcge0  14387  pcneg  14399  pcdvdstr  14401  pcz  14406  pcprmpw2  14407  pcadd  14410  ramcl2  14536  0ramcl  14543  ramub1lem1  14546  ramcl  14549  mrerintcl  15004  mreriincl  15005  mreexexlem4d  15054  mreclatBAD  15934  psgnunilem1  16635  odmulg  16695  sylow1lem1  16735  pgpfi  16742  odadd1  16971  odadd2  16972  gsumval3OLD  17025  gsumval3  17028  gsumpt  17102  gsumptOLD  17103  dprdfcntz  17162  dprdfcntzOLD  17168  dprd2da  17204  ablfac1eulem  17236  pgpfaclem3  17247  abvneg  17596  lssssr  17712  lspsneq  17881  lspdisj2  17886  drngnidl  17990  cnsubrg  18591  riinopn  19502  riincld  19630  neipeltop  19716  hauscmplem  19992  cmpfi  19994  ptbasfi  20167  xkoccn  20205  txindislem  20219  txtube  20226  hmphindis  20383  fclscmp  20616  utop2nei  20838  nrginvrcn  21285  nmoleub  21323  blcvx  21388  xrsxmet  21399  xrsblre  21401  lebnumlem3  21548  cphsqrtcl2  21718  ovollb2  21985  ioorcl  22071  i1fmulc  22195  itg1mulc  22196  mbfi1fseqlem4  22210  dvlip  22479  dvne0  22497  ig1pdvds  22662  plyeq0lem  22692  plyeq0  22693  aannenlem2  22810  aalioulem6  22818  abelthlem8  22919  abelth  22921  cxpexp  23136  cxpge0  23151  cxpmul2  23157  abscxp2  23161  abscxpbnd  23214  cxpeq  23218  nnlogbexp  23239  isosctrlem2  23269  atanrecl  23358  wilthlem2  23460  dchrabs2  23654  dchr1re  23655  lgsneg1  23712  lgsdirprm  23721  lgsdir  23722  lgsne0  23725  lgsdirnn0  23731  lgsdinn0  23732  2sqlem9  23765  rpvmasumlem  23789  dchrvmasumiflem1  23803  dchrisum0flblem1  23810  rpvmasum2  23814  pntrsumbnd2  23869  pntleml  23913  tgcgrextend  23996  tgbtwnexch2  24007  tgifscgr  24020  tgcolg  24061  tgidinside  24078  tgbtwnconn1lem2  24080  tgbtwnconn1lem3  24081  tglinethru  24136  tglnpt2  24141  tglineneq  24144  coltr  24147  coltr3  24149  colline  24150  mirreu3  24155  miriso  24170  mirln  24176  mirln2  24177  mirconn  24178  mirbtwnhl  24180  colmid  24185  krippenlem  24187  midexlem  24189  ragflat  24201  ragcgr  24204  perprag  24220  perpdragALT  24221  colperpexlem1  24224  colperpexlem3  24226  midex  24231  opphllem1  24239  opphllem2  24240  opphllem5  24243  opphllem6  24244  lmiisolem  24281  hypcgrlem1  24284  hypcgrlem2  24285  umgraex  24444  eupath2lem3  25100  nmcoplbi  27063  nmophmi  27066  nmbdfnlbi  27084  disjdifprg  27565  imadifxp  27591  xlt2addrd  27728  ssnnssfz  27750  locfinref  27998  esumpr2  28215  sigapildsyslem  28306  sigapildsys  28307  mbfmcst  28386  carsgsigalem  28442  carsgclctunlem3  28447  probun  28541  0rrv  28573  sgncl  28660  signsvtn0  28710  signstfvneq0  28712  btwnconn1lem11  29900  mblfinlem1  30216  mblfinlem2  30217  ismblfin  30220  itg2addnclem  30232  itgaddnclem2  30240  bddiblnc  30251  areacirclem4  30276  areacirc  30278  isbnd3  30446  blbnd  30449  rrnequiv  30497  jm2.19  31101  jm2.23  31104  lcmdvds  31382  nzss  31390  stoweidlem58  32006  fourierdlem41  32096  fourierdlem48  32103  fouriersw  32180  etransclem24  32207  ssnn0ssfz  33138  lsmsat  35146  lkrscss  35236  eqlkr  35237  lkrshpor  35245  atcvrj2b  35569  atltcvr  35572  3dim1  35604  3dim2  35605  3dim3  35606  ps-2  35615  2at0mat0  35662  dalemdnee  35803  dalem63  35872  lnatexN  35916  2llnma3r  35925  pmodlem1  35983  pmapjat1  35990  pclfinclN  36087  osumclN  36104  pexmidALTN  36115  lhpexle2lem  36146  lhpexle3lem  36148  4atexlemex6  36211  4atex  36213  trlnle  36324  trlval3  36325  cdlemc  36335  cdlemd9  36344  cdleme27N  36508  cdleme28c  36511  cdleme32fvaw  36578  cdleme42ke  36624  cdleme42keg  36625  cdleme42mgN  36627  cdleme17d  36637  cdleme48fvg  36639  cdleme50trn123  36693  cdlemb3  36745  cdlemg8  36770  cdlemg15a  36794  cdlemg15  36795  cdlemg16  36796  cdlemg16ALTN  36797  cdlemg16z  36798  cdlemg16zz  36799  cdlemg20  36824  cdlemg22  36826  cdlemg37  36828  cdlemg31d  36839  cdlemg39  36855  cdlemg40  36856  ltrncom  36877  tendotr  36969  cdlemk25-3  37043  cdlemk35s-id  37077  cdlemk39s-id  37079  cdlemk53b  37095  cdlemk53  37096  cdlemk55  37100  cdlemk35u  37103  cdlemk55u  37105  cdlemk39u  37107  cdlemk19u  37109  cdleml5N  37119  dia2dimlem7  37210  dia2dimlem13  37216  dih1dimatlem  37469  dihlsprn  37471  dihjat1lem  37568  dihjat1  37569  dvh2dim  37585  dochexmid  37608  lclkrlem1  37646  lclkrlem2i  37655  lclkrlem2t  37666  lcfrlem34  37716  lcfrlem38  37720  lcfrlem41  37723  mapdindp1  37860  mapdindp2  37861  mapdh6dN  37879  mapdh6jN  37885  mapdh8j  37928  mapdh8  37929  hdmap1l6d  37954  hdmap1l6j  37960  hdmap11lem2  37985  hdmap14lem7  38017