Theorem pm2.61dane 2738

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

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   =/= wne 2614

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 188  df-an 372  df-ne 2616

This theorem is referenced by:  pm2.61da2ne  2739  pm2.61da3ne  2740  pm2.61da3neOLD  2741  pm2.61iine  2742  disjxiun  4420  onfr  5481  f1oprswap  5870  soex  6750  riiner  7447  difsnen  7663  mapdom2  7752  nnunifi  7831  fofinf1o  7861  brwdom2  8097  cantnff  8187  cantnfp1  8194  carddomi2  8412  wdomfil  8499  fin1a2lem10  8846  fin1a2lem11  8847  uzsupss  11263  xaddcom  11538  xnegdi  11541  xpncan  11544  xleadd1a  11546  xsubge0  11554  cnpart  13303  fsumcllem  13797  fsumrev2  13842  expcnv  13921  geomulcvg  13931  fprodcllem  14004  fsumdvds  14347  gcd0id  14486  nn0seqcvgd  14528  lcmdvds  14572  mulgcddvds  14660  pcge0  14810  pcneg  14822  pcdvdstr  14824  pcz  14829  pcprmpw2  14830  pcadd  14833  ramcl2  14972  ramcl2OLD  14973  0ramcl  14980  ramub1lem1  14983  ramcl  14986  mrerintcl  15502  mreriincl  15503  mreexexlem4d  15552  mreclatBAD  16432  psgnunilem1  17133  odmulg  17206  sylow1lem1  17249  pgpfi  17256  odadd1  17485  odadd2  17486  gsumval3  17540  gsumpt  17593  dprdfcntz  17647  dprd2da  17674  ablfac1eulem  17704  pgpfaclem3  17715  abvneg  18061  lssssr  18175  lspsneq  18344  lspdisj2  18349  drngnidl  18452  cnsubrg  19027  riinopn  19936  riincld  20057  neipeltop  20143  hauscmplem  20419  cmpfi  20421  ptbasfi  20594  xkoccn  20632  txindislem  20646  txtube  20653  hmphindis  20810  fclscmp  21043  utop2nei  21263  nrginvrcn  21692  nmoleub  21734  nmoleubOLD  21750  blcvx  21814  xrsxmet  21825  xrsblre  21827  lebnumlem3  21989  lebnumlem3OLD  21992  cphsqrtcl2  22162  ovollb2  22440  ioorcl  22527  ioorclOLD  22532  i1fmulc  22659  itg1mulc  22660  mbfi1fseqlem4  22674  dvlip  22943  dvne0  22961  ig1pdvds  23126  ig1pdvdsOLD  23132  plyeq0lem  23162  plyeq0  23163  aannenlem2  23283  aalioulem6  23291  abelthlem8  23392  abelth  23394  cxpexp  23611  cxpge0  23626  cxpmul2  23632  abscxp2  23636  abscxpbnd  23691  cxpeq  23695  nnlogbexp  23716  isosctrlem2  23746  atanrecl  23835  wilthlem2  23992  dchrabs2  24188  dchr1re  24189  lgsneg1  24246  lgsdirprm  24255  lgsdir  24256  lgsne0  24259  lgsdirnn0  24265  lgsdinn0  24266  2sqlem9  24299  rpvmasumlem  24323  dchrvmasumiflem1  24337  dchrisum0flblem1  24344  rpvmasum2  24348  pntrsumbnd2  24403  pntleml  24447  tgcgrextend  24527  tgbtwnexch2  24538  tgifscgr  24551  tgcolg  24597  tgidinside  24614  tgbtwnconn1lem2  24616  tgbtwnconn1lem3  24617  lnhl  24658  tglinethru  24679  tglnpt2  24684  tglineneq  24687  coltr  24690  coltr3  24691  colline  24692  mirreu3  24697  miriso  24713  mirln  24719  mirln2  24720  mirconn  24721  mirbtwnhl  24723  colmid  24731  krippenlem  24733  midexlem  24735  ragflat  24747  ragcgr  24750  perprag  24766  perpdragALT  24767  colperpexlem1  24770  colperpexlem3  24772  midex  24777  opphllem1  24787  opphllem2  24788  opphllem5  24791  opphllem6  24792  hlpasch  24796  lmiisolem  24836  hypcgrlem1  24839  hypcgrlem2  24840  cgrg3col4  24882  umgraex  25048  eupath2lem3  25705  nmcoplbi  27679  nmophmi  27682  nmbdfnlbi  27700  disjdifprg  28187  imadifxp  28214  xlt2addrd  28344  ssnnssfz  28373  psgnfzto1stlem  28621  locfinref  28676  esumpr2  28896  unelldsys  28988  sigapildsyslem  28991  sigapildsys  28992  mbfmcst  29089  carsgsigalem  29155  carsgclctunlem3  29160  pmeasmono  29165  probun  29260  0rrv  29292  sgncl  29417  signsvtn0  29467  signstfvneq0  29469  btwnconn1lem11  30869  finxp00  31758  poimirlem14  31918  mblfinlem1  31941  mblfinlem2  31942  ismblfin  31945  itg2addnclem  31957  itgaddnclem2  31965  bddiblnc  31976  areacirclem4  31999  areacirc  32001  isbnd3  32080  blbnd  32083  rrnequiv  32131  lsmsat  32543  lkrscss  32633  eqlkr  32634  lkrshpor  32642  atcvrj2b  32966  atltcvr  32969  3dim1  33001  3dim2  33002  3dim3  33003  ps-2  33012  2at0mat0  33059  dalemdnee  33200  dalem63  33269  lnatexN  33313  2llnma3r  33322  pmodlem1  33380  pmapjat1  33387  pclfinclN  33484  osumclN  33501  pexmidALTN  33512  lhpexle2lem  33543  lhpexle3lem  33545  4atexlemex6  33608  4atex  33610  trlnle  33721  trlval3  33722  cdlemc  33732  cdlemd9  33741  cdleme27N  33905  cdleme28c  33908  cdleme32fvaw  33975  cdleme42ke  34021  cdleme42keg  34022  cdleme42mgN  34024  cdleme17d  34034  cdleme48fvg  34036  cdleme50trn123  34090  cdlemb3  34142  cdlemg8  34167  cdlemg15a  34191  cdlemg15  34192  cdlemg16  34193  cdlemg16ALTN  34194  cdlemg16z  34195  cdlemg16zz  34196  cdlemg20  34221  cdlemg22  34223  cdlemg37  34225  cdlemg31d  34236  cdlemg39  34252  cdlemg40  34253  ltrncom  34274  tendotr  34366  cdlemk25-3  34440  cdlemk35s-id  34474  cdlemk39s-id  34476  cdlemk53b  34492  cdlemk53  34493  cdlemk55  34497  cdlemk35u  34500  cdlemk55u  34502  cdlemk39u  34504  cdlemk19u  34506  cdleml5N  34516  dia2dimlem7  34607  dia2dimlem13  34613  dih1dimatlem  34866  dihlsprn  34868  dihjat1lem  34965  dihjat1  34966  dvh2dim  34982  dochexmid  35005  lclkrlem1  35043  lclkrlem2i  35052  lclkrlem2t  35063  lcfrlem34  35113  lcfrlem38  35117  lcfrlem41  35120  mapdindp1  35257  mapdindp2  35258  mapdh6dN  35276  mapdh6jN  35282  mapdh8j  35325  mapdh8  35326  hdmap1l6d  35351  hdmap1l6j  35357  hdmap11lem2  35382  hdmap14lem7  35414  jm2.19  35818  jm2.23  35821  nzss  36636  stoweidlem58  37859  fourierdlem41  37951  fourierdlem48  37958  fouriersw  38035  etransclem24  38063  umgrex  39012  ssnn0ssfz  39752