Theorem pm2.61dane 2749

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

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

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 2627

This theorem is referenced by:  pm2.61da2ne  2750  pm2.61da3ne  2751  pm2.61da3neOLD  2752  pm2.61iine  2753  disjxiun  4423  onfr  5481  f1oprswap  5870  soex  6750  riiner  7444  difsnen  7660  mapdom2  7749  nnunifi  7828  fofinf1o  7858  brwdom2  8088  cantnff  8178  cantnfp1  8185  carddomi2  8403  wdomfil  8490  fin1a2lem10  8837  fin1a2lem11  8838  uzsupss  11256  xaddcom  11531  xnegdi  11534  xpncan  11537  xleadd1a  11539  xsubge0  11547  cnpart  13282  fsumcllem  13776  fsumrev2  13821  expcnv  13900  geomulcvg  13910  fprodcllem  13983  fsumdvds  14326  gcd0id  14461  nn0seqcvgd  14500  lcmdvds  14538  mulgcddvds  14623  pcge0  14765  pcneg  14777  pcdvdstr  14779  pcz  14784  pcprmpw2  14785  pcadd  14788  ramcl2  14927  ramcl2OLD  14928  0ramcl  14935  ramub1lem1  14938  ramcl  14941  mrerintcl  15445  mreriincl  15446  mreexexlem4d  15495  mreclatBAD  16375  psgnunilem1  17076  odmulg  17136  sylow1lem1  17176  pgpfi  17183  odadd1  17412  odadd2  17413  gsumval3  17467  gsumpt  17520  dprdfcntz  17574  dprd2da  17601  ablfac1eulem  17631  pgpfaclem3  17642  abvneg  17988  lssssr  18102  lspsneq  18271  lspdisj2  18276  drngnidl  18379  cnsubrg  18954  riinopn  19860  riincld  19981  neipeltop  20067  hauscmplem  20343  cmpfi  20345  ptbasfi  20518  xkoccn  20556  txindislem  20570  txtube  20577  hmphindis  20734  fclscmp  20967  utop2nei  21187  nrginvrcn  21616  nmoleub  21654  blcvx  21718  xrsxmet  21729  xrsblre  21731  lebnumlem3  21878  cphsqrtcl2  22048  ovollb2  22311  ioorcl  22397  ioorclOLD  22402  i1fmulc  22529  itg1mulc  22530  mbfi1fseqlem4  22544  dvlip  22813  dvne0  22831  ig1pdvds  22993  plyeq0lem  23023  plyeq0  23024  aannenlem2  23141  aalioulem6  23149  abelthlem8  23250  abelth  23252  cxpexp  23469  cxpge0  23484  cxpmul2  23490  abscxp2  23494  abscxpbnd  23549  cxpeq  23553  nnlogbexp  23574  isosctrlem2  23604  atanrecl  23693  wilthlem2  23850  dchrabs2  24044  dchr1re  24045  lgsneg1  24102  lgsdirprm  24111  lgsdir  24112  lgsne0  24115  lgsdirnn0  24121  lgsdinn0  24122  2sqlem9  24155  rpvmasumlem  24179  dchrvmasumiflem1  24193  dchrisum0flblem1  24200  rpvmasum2  24204  pntrsumbnd2  24259  pntleml  24303  tgcgrextend  24383  tgbtwnexch2  24394  tgifscgr  24407  tgcolg  24450  tgidinside  24467  tgbtwnconn1lem2  24469  tgbtwnconn1lem3  24470  tglinethru  24531  tglnpt2  24536  tglineneq  24539  coltr  24542  coltr3  24544  colline  24545  mirreu3  24550  miriso  24565  mirln  24571  mirln2  24572  mirconn  24573  mirbtwnhl  24575  colmid  24581  krippenlem  24583  midexlem  24585  ragflat  24597  ragcgr  24600  perprag  24616  perpdragALT  24617  colperpexlem1  24620  colperpexlem3  24622  midex  24627  opphllem1  24637  opphllem2  24638  opphllem5  24641  opphllem6  24642  lmiisolem  24685  hypcgrlem1  24688  hypcgrlem2  24689  umgraex  24887  eupath2lem3  25543  nmcoplbi  27507  nmophmi  27510  nmbdfnlbi  27528  disjdifprg  28015  imadifxp  28042  xlt2addrd  28170  ssnnssfz  28194  psgnfzto1stlem  28443  locfinref  28498  esumpr2  28718  unelldsys  28810  sigapildsyslem  28813  sigapildsys  28814  mbfmcst  28911  carsgsigalem  28967  carsgclctunlem3  28972  pmeasmono  28976  probun  29069  0rrv  29101  sgncl  29188  signsvtn0  29238  signstfvneq0  29240  btwnconn1lem11  30640  poimirlem14  31648  mblfinlem1  31671  mblfinlem2  31672  ismblfin  31675  itg2addnclem  31687  itgaddnclem2  31695  bddiblnc  31706  areacirclem4  31729  areacirc  31731  isbnd3  31810  blbnd  31813  rrnequiv  31861  lsmsat  32273  lkrscss  32363  eqlkr  32364  lkrshpor  32372  atcvrj2b  32696  atltcvr  32699  3dim1  32731  3dim2  32732  3dim3  32733  ps-2  32742  2at0mat0  32789  dalemdnee  32930  dalem63  32999  lnatexN  33043  2llnma3r  33052  pmodlem1  33110  pmapjat1  33117  pclfinclN  33214  osumclN  33231  pexmidALTN  33242  lhpexle2lem  33273  lhpexle3lem  33275  4atexlemex6  33338  4atex  33340  trlnle  33451  trlval3  33452  cdlemc  33462  cdlemd9  33471  cdleme27N  33635  cdleme28c  33638  cdleme32fvaw  33705  cdleme42ke  33751  cdleme42keg  33752  cdleme42mgN  33754  cdleme17d  33764  cdleme48fvg  33766  cdleme50trn123  33820  cdlemb3  33872  cdlemg8  33897  cdlemg15a  33921  cdlemg15  33922  cdlemg16  33923  cdlemg16ALTN  33924  cdlemg16z  33925  cdlemg16zz  33926  cdlemg20  33951  cdlemg22  33953  cdlemg37  33955  cdlemg31d  33966  cdlemg39  33982  cdlemg40  33983  ltrncom  34004  tendotr  34096  cdlemk25-3  34170  cdlemk35s-id  34204  cdlemk39s-id  34206  cdlemk53b  34222  cdlemk53  34223  cdlemk55  34227  cdlemk35u  34230  cdlemk55u  34232  cdlemk39u  34234  cdlemk19u  34236  cdleml5N  34246  dia2dimlem7  34337  dia2dimlem13  34343  dih1dimatlem  34596  dihlsprn  34598  dihjat1lem  34695  dihjat1  34696  dvh2dim  34712  dochexmid  34735  lclkrlem1  34773  lclkrlem2i  34782  lclkrlem2t  34793  lcfrlem34  34843  lcfrlem38  34847  lcfrlem41  34850  mapdindp1  34987  mapdindp2  34988  mapdh6dN  35006  mapdh6jN  35012  mapdh8j  35055  mapdh8  35056  hdmap1l6d  35081  hdmap1l6j  35087  hdmap11lem2  35112  hdmap14lem7  35144  jm2.19  35544  jm2.23  35547  nzss  36293  stoweidlem58  37478  fourierdlem41  37569  fourierdlem48  37576  fouriersw  37653  etransclem24  37680  ssnn0ssfz  38880