Theorem pm2.61dane 2679

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 2678	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1362   =/= wne 2596

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 2598

This theorem is referenced by:  pm2.61da2ne  2680  pm2.61da3ne  2681  disjxiun  4277  onfr  4745  f1oprswap  5668  soex  6510  riiner  7161  difsnen  7381  mapdom2  7470  nnunifi  7551  fofinf1o  7580  brwdom2  7776  cantnff  7870  cantnfp1  7877  cantnfp1OLD  7903  carddomi2  8128  wdomfil  8219  fin1a2lem10  8566  fin1a2lem11  8567  uzsupss  10934  xaddcom  11195  xnegdi  11198  xpncan  11201  xleadd1a  11203  xsubge0  11211  cnpart  12712  fsumcllem  13192  fsumrev2  13231  expcnv  13308  geomulcvg  13318  fsumdvds  13558  gcd0id  13689  nn0seqcvgd  13727  mulgcddvds  13772  pcge0  13910  pcneg  13922  pcdvdstr  13924  pcz  13929  pcprmpw2  13930  pcadd  13933  ramcl2  14059  0ramcl  14066  ramub1lem1  14069  ramcl  14072  mrerintcl  14517  mreriincl  14518  mreexexlem4d  14567  mreclatBAD  15339  psgnunilem1  15978  odmulg  16036  sylow1lem1  16076  pgpfi  16083  odadd1  16309  odadd2  16310  gsumval3OLD  16361  gsumval3  16364  gsumpt  16428  gsumptOLD  16429  dprdfcntz  16472  dprdfcntzOLD  16478  dprd2da  16514  ablfac1eulem  16546  pgpfaclem3  16557  abvneg  16842  lssssr  16955  lspsneq  17124  lspdisj2  17129  drngnidl  17232  cnsubrg  17716  riinopn  18362  riincld  18489  neipeltop  18574  hauscmplem  18850  cmpfi  18852  ptbasfi  18995  xkoccn  19033  txindislem  19047  txtube  19054  hmphindis  19211  fclscmp  19444  utop2nei  19666  nrginvrcn  20113  nmoleub  20151  blcvx  20216  xrsxmet  20227  xrsblre  20229  lebnumlem3  20376  cphsqrcl2  20546  ovollb2  20813  ioorcl  20898  i1fmulc  21022  itg1mulc  21023  mbfi1fseqlem4  21037  dvlip  21306  dvne0  21324  ig1pdvds  21532  plyeq0lem  21562  plyeq0  21563  aannenlem2  21679  aalioulem6  21687  abelthlem8  21788  abelth  21790  cxpexp  21997  cxpge0  22012  cxpmul2  22018  abscxp2  22022  abscxpbnd  22075  cxpeq  22079  isosctrlem2  22101  atanrecl  22190  wilthlem2  22291  dchrabs2  22485  dchr1re  22486  lgsneg1  22543  lgsdirprm  22552  lgsdir  22553  lgsne0  22556  lgsdirnn0  22562  lgsdinn0  22563  2sqlem9  22596  rpvmasumlem  22620  dchrvmasumiflem1  22634  dchrisum0flblem1  22641  rpvmasum2  22645  pntrsumbnd2  22700  pntleml  22744  tgcolg  22866  tgidinside  22878  tgbtwnconn1lem2  22880  tgbtwnconn1lem3  22881  tglinethru  22912  colline  22917  mirreu3  22923  miriso  22934  umgraex  23079  eupath2lem3  23422  nmcoplbi  25254  nmophmi  25257  nmbdfnlbi  25275  disjdifprg  25742  imadifxp  25762  xlt2addrd  25875  ssnnssfz  25898  nnlogbexp  26316  esumpr2  26370  mbfmcst  26527  probun  26649  0rrv  26681  sgncl  26768  fprodcllem  27310  btwnconn1lem11  27974  mblfinlem1  28269  mblfinlem2  28270  ismblfin  28273  itg2addnclem  28284  itgaddnclem2  28292  bddiblnc  28303  areacirclem4  28328  areacirc  28330  isbnd3  28524  blbnd  28527  rrnequiv  28575  jm2.19  29184  jm2.23  29187  stoweidlem58  29696  lsmsat  32223  lkrscss  32313  eqlkr  32314  lkrshpor  32322  atcvrj2b  32646  atltcvr  32649  3dim1  32681  3dim2  32682  3dim3  32683  ps-2  32692  2at0mat0  32739  dalemdnee  32880  dalem63  32949  lnatexN  32993  2llnma3r  33002  pmodlem1  33060  pmapjat1  33067  pclfinclN  33164  osumclN  33181  pexmidALTN  33192  lhpexle2lem  33223  lhpexle3lem  33225  4atexlemex6  33288  4atex  33290  trlnle  33400  trlval3  33401  cdlemc  33411  cdlemd9  33420  cdleme27N  33583  cdleme28c  33586  cdleme32fvaw  33653  cdleme42ke  33699  cdleme42keg  33700  cdleme42mgN  33702  cdleme17d  33712  cdleme48fvg  33714  cdleme50trn123  33768  cdlemb3  33820  cdlemg8  33845  cdlemg15a  33869  cdlemg15  33870  cdlemg16  33871  cdlemg16ALTN  33872  cdlemg16z  33873  cdlemg16zz  33874  cdlemg20  33899  cdlemg22  33901  cdlemg37  33903  cdlemg31d  33914  cdlemg39  33930  cdlemg40  33931  ltrncom  33952  tendotr  34044  cdlemk25-3  34118  cdlemk35s-id  34152  cdlemk39s-id  34154  cdlemk53b  34170  cdlemk53  34171  cdlemk55  34175  cdlemk35u  34178  cdlemk55u  34180  cdlemk39u  34182  cdlemk19u  34184  cdleml5N  34194  dia2dimlem7  34285  dia2dimlem13  34291  dih1dimatlem  34544  dihlsprn  34546  dihjat1lem  34643  dihjat1  34644  dvh2dim  34660  dochexmid  34683  lclkrlem1  34721  lclkrlem2i  34730  lclkrlem2t  34741  lcfrlem34  34791  lcfrlem38  34795  lcfrlem41  34798  mapdindp1  34935  mapdindp2  34936  mapdh6dN  34954  mapdh6jN  34960  mapdh8j  35003  mapdh8  35004  hdmap1l6d  35029  hdmap1l6j  35035  hdmap11lem2  35060  hdmap14lem7  35092