Theorem pm2.61dane 2881

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

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   =/= wne 2794

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 197  df-an 386  df-ne 2795

This theorem is referenced by:  pm2.61da2ne  2882  pm2.61da3ne  2883  pm2.61iine  2884  disjxiun  4649  disjxiunOLD  4650  onfr  5763  f1oprswap  6180  soex  7109  riiner  7820  difsnen  8042  mapdom2  8131  nnunifi  8211  fofinf1o  8241  brwdom2  8478  cantnff  8571  cantnfp1  8578  carddomi2  8796  wdomfil  8884  fin1a2lem10  9231  fin1a2lem11  9232  uzsupss  11780  xaddcom  12071  xnegdi  12078  xpncan  12081  xleadd1a  12083  xsubge0  12091  cnpart  13980  fsumcllem  14463  fsumrev2  14514  expcnv  14596  geomulcvg  14607  fprodcllem  14681  fsumdvds  15030  gcd0id  15240  nn0seqcvgd  15283  lcmdvds  15321  mulgcddvds  15369  pcge0  15566  pcneg  15578  pcdvdstr  15580  pcz  15585  pcprmpw2  15586  pcadd  15593  ramcl2  15720  0ramcl  15727  ramub1lem1  15730  ramcl  15733  mrerintcl  16257  mreriincl  16258  mreexexlem4d  16307  mreclatBAD  17187  psgnunilem1  17913  odmulg  17973  sylow1lem1  18013  pgpfi  18020  odadd1  18251  odadd2  18252  gsumval3  18308  gsumpt  18361  dprdfcntz  18414  dprd2da  18441  ablfac1eulem  18471  pgpfaclem3  18482  abvneg  18834  lssssr  18953  lspsneq  19122  lspdisj2  19127  drngnidl  19229  cnsubrg  19806  riinopn  20713  riincld  20848  neipeltop  20933  hauscmplem  21209  cmpfi  21211  ptbasfi  21384  xkoccn  21422  txindislem  21436  txtube  21443  hmphindis  21600  fclscmp  21834  utop2nei  22054  nrginvrcn  22496  nmoleub  22535  blcvx  22601  xrsxmet  22612  xrsblre  22614  lebnumlem3  22762  cphsqrtcl2  22986  ovollb2  23257  ioorcl  23345  i1fmulc  23470  itg1mulc  23471  mbfi1fseqlem4  23485  dvlip  23756  dvne0  23774  ig1pdvds  23936  plyeq0lem  23966  plyeq0  23967  aannenlem2  24084  aalioulem6  24092  abelthlem8  24193  abelth  24195  cxpexp  24414  cxpge0  24429  cxpmul2  24435  abscxp2  24439  abscxpbnd  24494  cxpeq  24498  nnlogbexp  24519  isosctrlem2  24549  atanrecl  24638  wilthlem2  24795  dchrabs2  24987  dchr1re  24988  lgsneg1  25047  lgsdirprm  25056  lgsdir  25057  lgsne0  25060  lgsdirnn0  25069  lgsdinn0  25070  2sqlem9  25152  rpvmasumlem  25176  dchrvmasumiflem1  25190  dchrisum0flblem1  25197  rpvmasum2  25201  pntrsumbnd2  25256  pntleml  25300  tgcgrextend  25380  tgbtwnexch2  25391  tgifscgr  25403  tgcolg  25449  tgidinside  25466  tgbtwnconn1lem2  25468  tgbtwnconn1lem3  25469  lnhl  25510  tglinethru  25531  tglnpt2  25536  tglineneq  25539  coltr  25542  coltr3  25543  colline  25544  mirreu3  25549  miriso  25565  mirln  25571  mirln2  25572  mirconn  25573  mirbtwnhl  25575  colmid  25583  krippenlem  25585  midexlem  25587  ragflat  25599  ragcgr  25602  perprag  25618  perpdragALT  25619  colperpexlem1  25622  colperpexlem3  25624  midex  25629  opphllem1  25639  opphllem2  25640  opphllem5  25643  opphllem6  25644  hlpasch  25648  lmiisolem  25688  hypcgrlem1  25691  hypcgrlem2  25692  cgrg3col4  25734  upgrex  25987  crctcshwlk  26714  crctcsh  26716  1wlkdlem2  26998  eupth2lem3lem3  27090  eupth2lem3lem7  27094  nmcoplbi  28887  nmophmi  28890  nmbdfnlbi  28908  disjdifprg  29388  imadifxp  29414  xlt2addrd  29523  ssnnssfz  29549  psgnfzto1stlem  29850  pmtridf1o  29856  pmtridfv1  29857  pmtridfv2  29858  locfinref  29908  esumpr2  30129  unelldsys  30221  sigapildsyslem  30224  sigapildsys  30225  mbfmcst  30321  carsgsigalem  30377  carsgclctunlem3  30382  pmeasmono  30386  probun  30481  0rrv  30513  sgncl  30600  signsvtn0  30647  signstfvneq0  30649  btwnconn1lem11  32204  finxp00  33239  matunitlindf  33407  poimirlem14  33423  mblfinlem1  33446  mblfinlem2  33447  ismblfin  33450  itg2addnclem  33461  itgaddnclem2  33469  bddiblnc  33480  areacirclem4  33503  areacirc  33505  isbnd3  33583  blbnd  33586  rrnequiv  33634  lsmsat  34295  lkrscss  34385  eqlkr  34386  lkrshpor  34394  atcvrj2b  34718  atltcvr  34721  3dim1  34753  3dim2  34754  3dim3  34755  ps-2  34764  2at0mat0  34811  dalemdnee  34952  dalem63  35021  lnatexN  35065  2llnma3r  35074  pmodlem1  35132  pmapjat1  35139  pclfinclN  35236  osumclN  35253  pexmidALTN  35264  lhpexle2lem  35295  lhpexle3lem  35297  4atexlemex6  35360  4atex  35362  trlnle  35473  trlval3  35474  cdlemc  35484  cdlemd9  35493  cdleme27N  35657  cdleme28c  35660  cdleme32fvaw  35727  cdleme42ke  35773  cdleme42keg  35774  cdleme42mgN  35776  cdleme17d  35786  cdleme48fvg  35788  cdleme50trn123  35842  cdlemb3  35894  cdlemg8  35919  cdlemg15a  35943  cdlemg15  35944  cdlemg16  35945  cdlemg16ALTN  35946  cdlemg16z  35947  cdlemg16zz  35948  cdlemg20  35973  cdlemg22  35975  cdlemg37  35977  cdlemg31d  35988  cdlemg39  36004  cdlemg40  36005  ltrncom  36026  tendotr  36118  cdlemk25-3  36192  cdlemk35s-id  36226  cdlemk39s-id  36228  cdlemk53b  36244  cdlemk53  36245  cdlemk55  36249  cdlemk35u  36252  cdlemk55u  36254  cdlemk39u  36256  cdlemk19u  36258  cdleml5N  36268  dia2dimlem7  36359  dia2dimlem13  36365  dih1dimatlem  36618  dihlsprn  36620  dihjat1lem  36717  dihjat1  36718  dvh2dim  36734  dochexmid  36757  lclkrlem1  36795  lclkrlem2i  36804  lclkrlem2t  36815  lcfrlem34  36865  lcfrlem38  36869  lcfrlem41  36872  mapdindp1  37009  mapdindp2  37010  mapdh6dN  37028  mapdh6jN  37034  mapdh8j  37077  mapdh8  37078  hdmap1l6d  37103  hdmap1l6j  37109  hdmap11lem2  37134  hdmap14lem7  37166  jm2.19  37560  jm2.23  37563  nzss  38516  cnrefiisplem  40055  stoweidlem58  40275  fourierdlem41  40365  fourierdlem48  40371  fouriersw  40448  etransclem24  40475  nnfoctbdjlem  40672  ssnn0ssfz  42127