Theorem pm2.61dane 2713

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   =/= wne 2620

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 2622

This theorem is referenced by:  pm2.61da2ne  2714  pm2.61da3ne  2715  disjxiun  4310  onfr  4779  f1oprswap  5701  soex  6542  riiner  7194  difsnen  7414  mapdom2  7503  nnunifi  7584  fofinf1o  7613  brwdom2  7809  cantnff  7903  cantnfp1  7910  cantnfp1OLD  7936  carddomi2  8161  wdomfil  8252  fin1a2lem10  8599  fin1a2lem11  8600  uzsupss  10968  xaddcom  11229  xnegdi  11232  xpncan  11235  xleadd1a  11237  xsubge0  11245  cnpart  12750  fsumcllem  13230  fsumrev2  13270  expcnv  13347  geomulcvg  13357  fsumdvds  13597  gcd0id  13728  nn0seqcvgd  13766  mulgcddvds  13811  pcge0  13949  pcneg  13961  pcdvdstr  13963  pcz  13968  pcprmpw2  13969  pcadd  13972  ramcl2  14098  0ramcl  14105  ramub1lem1  14108  ramcl  14111  mrerintcl  14556  mreriincl  14557  mreexexlem4d  14606  mreclatBAD  15378  psgnunilem1  16020  odmulg  16078  sylow1lem1  16118  pgpfi  16125  odadd1  16351  odadd2  16352  gsumval3OLD  16403  gsumval3  16406  gsumpt  16476  gsumptOLD  16477  dprdfcntz  16521  dprdfcntzOLD  16527  dprd2da  16563  ablfac1eulem  16595  pgpfaclem3  16606  abvneg  16941  lssssr  17056  lspsneq  17225  lspdisj2  17230  drngnidl  17333  cnsubrg  17895  riinopn  18543  riincld  18670  neipeltop  18755  hauscmplem  19031  cmpfi  19033  ptbasfi  19176  xkoccn  19214  txindislem  19228  txtube  19235  hmphindis  19392  fclscmp  19625  utop2nei  19847  nrginvrcn  20294  nmoleub  20332  blcvx  20397  xrsxmet  20408  xrsblre  20410  lebnumlem3  20557  cphsqrcl2  20727  ovollb2  20994  ioorcl  21079  i1fmulc  21203  itg1mulc  21204  mbfi1fseqlem4  21218  dvlip  21487  dvne0  21505  ig1pdvds  21670  plyeq0lem  21700  plyeq0  21701  aannenlem2  21817  aalioulem6  21825  abelthlem8  21926  abelth  21928  cxpexp  22135  cxpge0  22150  cxpmul2  22156  abscxp2  22160  abscxpbnd  22213  cxpeq  22217  isosctrlem2  22239  atanrecl  22328  wilthlem2  22429  dchrabs2  22623  dchr1re  22624  lgsneg1  22681  lgsdirprm  22690  lgsdir  22691  lgsne0  22694  lgsdirnn0  22700  lgsdinn0  22701  2sqlem9  22734  rpvmasumlem  22758  dchrvmasumiflem1  22772  dchrisum0flblem1  22779  rpvmasum2  22783  pntrsumbnd2  22838  pntleml  22882  tgcolg  23010  tgidinside  23025  tgbtwnconn1lem2  23027  tgbtwnconn1lem3  23028  tglinethru  23064  tglnpt2  23068  tglineneq  23071  colline  23074  mirreu3  23080  miriso  23095  colmid  23104  krippenlem  23106  midexlem  23108  ragflat  23120  ragcgr  23123  perprag  23133  colperplem1  23134  umgraex  23279  eupath2lem3  23622  nmcoplbi  25454  nmophmi  25457  nmbdfnlbi  25475  disjdifprg  25941  imadifxp  25961  xlt2addrd  26073  ssnnssfz  26098  nnlogbexp  26485  esumpr2  26539  mbfmcst  26696  probun  26824  0rrv  26856  sgncl  26943  fprodcllem  27486  btwnconn1lem11  28150  mblfinlem1  28454  mblfinlem2  28455  ismblfin  28458  itg2addnclem  28469  itgaddnclem2  28477  bddiblnc  28488  areacirclem4  28513  areacirc  28515  isbnd3  28709  blbnd  28712  rrnequiv  28760  jm2.19  29368  jm2.23  29371  stoweidlem58  29879  ssnn0ssfz  30770  lsmsat  32749  lkrscss  32839  eqlkr  32840  lkrshpor  32848  atcvrj2b  33172  atltcvr  33175  3dim1  33207  3dim2  33208  3dim3  33209  ps-2  33218  2at0mat0  33265  dalemdnee  33406  dalem63  33475  lnatexN  33519  2llnma3r  33528  pmodlem1  33586  pmapjat1  33593  pclfinclN  33690  osumclN  33707  pexmidALTN  33718  lhpexle2lem  33749  lhpexle3lem  33751  4atexlemex6  33814  4atex  33816  trlnle  33926  trlval3  33927  cdlemc  33937  cdlemd9  33946  cdleme27N  34109  cdleme28c  34112  cdleme32fvaw  34179  cdleme42ke  34225  cdleme42keg  34226  cdleme42mgN  34228  cdleme17d  34238  cdleme48fvg  34240  cdleme50trn123  34294  cdlemb3  34346  cdlemg8  34371  cdlemg15a  34395  cdlemg15  34396  cdlemg16  34397  cdlemg16ALTN  34398  cdlemg16z  34399  cdlemg16zz  34400  cdlemg20  34425  cdlemg22  34427  cdlemg37  34429  cdlemg31d  34440  cdlemg39  34456  cdlemg40  34457  ltrncom  34478  tendotr  34570  cdlemk25-3  34644  cdlemk35s-id  34678  cdlemk39s-id  34680  cdlemk53b  34696  cdlemk53  34697  cdlemk55  34701  cdlemk35u  34704  cdlemk55u  34706  cdlemk39u  34708  cdlemk19u  34710  cdleml5N  34720  dia2dimlem7  34811  dia2dimlem13  34817  dih1dimatlem  35070  dihlsprn  35072  dihjat1lem  35169  dihjat1  35170  dvh2dim  35186  dochexmid  35209  lclkrlem1  35247  lclkrlem2i  35256  lclkrlem2t  35267  lcfrlem34  35317  lcfrlem38  35321  lcfrlem41  35324  mapdindp1  35461  mapdindp2  35462  mapdh6dN  35480  mapdh6jN  35486  mapdh8j  35529  mapdh8  35530  hdmap1l6d  35555  hdmap1l6j  35561  hdmap11lem2  35586  hdmap14lem7  35618