Theorem pm2.61dane 2761

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1383   =/= wne 2638

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 2640

This theorem is referenced by:  pm2.61da2ne  2762  pm2.61da3ne  2763  pm2.61da3neOLD  2764  pm2.61iine  2765  disjxiun  4434  onfr  4907  f1oprswap  5845  soex  6728  riiner  7386  difsnen  7601  mapdom2  7690  nnunifi  7773  fofinf1o  7803  brwdom2  8002  cantnff  8096  cantnfp1  8103  cantnfp1OLD  8129  carddomi2  8354  wdomfil  8445  fin1a2lem10  8792  fin1a2lem11  8793  uzsupss  11185  xaddcom  11448  xnegdi  11451  xpncan  11454  xleadd1a  11456  xsubge0  11464  cnpart  13055  fsumcllem  13536  fsumrev2  13579  expcnv  13657  geomulcvg  13667  fprodcllem  13740  fsumdvds  14011  gcd0id  14143  nn0seqcvgd  14181  mulgcddvds  14227  pcge0  14367  pcneg  14379  pcdvdstr  14381  pcz  14386  pcprmpw2  14387  pcadd  14390  ramcl2  14516  0ramcl  14523  ramub1lem1  14526  ramcl  14529  mrerintcl  14976  mreriincl  14977  mreexexlem4d  15026  mreclatBAD  15796  psgnunilem1  16497  odmulg  16557  sylow1lem1  16597  pgpfi  16604  odadd1  16833  odadd2  16834  gsumval3OLD  16887  gsumval3  16890  gsumpt  16967  gsumptOLD  16968  dprdfcntz  17028  dprdfcntzOLD  17034  dprd2da  17070  ablfac1eulem  17102  pgpfaclem3  17113  abvneg  17462  lssssr  17578  lspsneq  17747  lspdisj2  17752  drngnidl  17856  cnsubrg  18457  riinopn  19395  riincld  19523  neipeltop  19608  hauscmplem  19884  cmpfi  19886  ptbasfi  20060  xkoccn  20098  txindislem  20112  txtube  20119  hmphindis  20276  fclscmp  20509  utop2nei  20731  nrginvrcn  21178  nmoleub  21216  blcvx  21281  xrsxmet  21292  xrsblre  21294  lebnumlem3  21441  cphsqrtcl2  21611  ovollb2  21878  ioorcl  21964  i1fmulc  22088  itg1mulc  22089  mbfi1fseqlem4  22103  dvlip  22372  dvne0  22390  ig1pdvds  22555  plyeq0lem  22585  plyeq0  22586  aannenlem2  22703  aalioulem6  22711  abelthlem8  22812  abelth  22814  cxpexp  23027  cxpge0  23042  cxpmul2  23048  abscxp2  23052  abscxpbnd  23105  cxpeq  23109  isosctrlem2  23131  atanrecl  23220  wilthlem2  23321  dchrabs2  23515  dchr1re  23516  lgsneg1  23573  lgsdirprm  23582  lgsdir  23583  lgsne0  23586  lgsdirnn0  23592  lgsdinn0  23593  2sqlem9  23626  rpvmasumlem  23650  dchrvmasumiflem1  23664  dchrisum0flblem1  23671  rpvmasum2  23675  pntrsumbnd2  23730  pntleml  23774  tgcgrextend  23854  tgbtwnexch2  23865  tgifscgr  23878  tgcolg  23919  tgidinside  23936  tgbtwnconn1lem2  23938  tgbtwnconn1lem3  23939  tglinethru  23994  tglnpt2  23999  tglineneq  24002  coltr  24005  coltr3  24007  colline  24008  mirreu3  24013  miriso  24028  mirln  24034  mirln2  24035  mirconn  24036  mirbtwnhl  24038  colmid  24043  krippenlem  24045  midexlem  24047  ragflat  24059  ragcgr  24062  perprag  24078  perpdragALT  24079  colperpexlem1  24082  colperpexlem3  24084  midex  24089  opphllem1  24097  opphllem2  24098  opphllem5  24101  opphllem6  24102  lmiisolem  24139  hypcgrlem1  24142  hypcgrlem2  24143  umgraex  24301  eupath2lem3  24957  nmcoplbi  26925  nmophmi  26928  nmbdfnlbi  26946  disjdifprg  27414  imadifxp  27436  xlt2addrd  27556  ssnnssfz  27575  locfinref  27822  nnlogbexp  27998  esumpr2  28052  mbfmcst  28208  probun  28336  0rrv  28368  sgncl  28455  signsvtn0  28505  signstfvneq0  28507  btwnconn1lem11  29723  mblfinlem1  30027  mblfinlem2  30028  ismblfin  30031  itg2addnclem  30042  itgaddnclem2  30050  bddiblnc  30061  areacirclem4  30086  areacirc  30088  isbnd3  30256  blbnd  30259  rrnequiv  30307  jm2.19  30911  jm2.23  30914  lcmdvds  31190  nzss  31198  stoweidlem58  31794  fourierdlem41  31884  fourierdlem48  31891  fouriersw  31968  ssnn0ssfz  32806  lsmsat  34608  lkrscss  34698  eqlkr  34699  lkrshpor  34707  atcvrj2b  35031  atltcvr  35034  3dim1  35066  3dim2  35067  3dim3  35068  ps-2  35077  2at0mat0  35124  dalemdnee  35265  dalem63  35334  lnatexN  35378  2llnma3r  35387  pmodlem1  35445  pmapjat1  35452  pclfinclN  35549  osumclN  35566  pexmidALTN  35577  lhpexle2lem  35608  lhpexle3lem  35610  4atexlemex6  35673  4atex  35675  trlnle  35786  trlval3  35787  cdlemc  35797  cdlemd9  35806  cdleme27N  35970  cdleme28c  35973  cdleme32fvaw  36040  cdleme42ke  36086  cdleme42keg  36087  cdleme42mgN  36089  cdleme17d  36099  cdleme48fvg  36101  cdleme50trn123  36155  cdlemb3  36207  cdlemg8  36232  cdlemg15a  36256  cdlemg15  36257  cdlemg16  36258  cdlemg16ALTN  36259  cdlemg16z  36260  cdlemg16zz  36261  cdlemg20  36286  cdlemg22  36288  cdlemg37  36290  cdlemg31d  36301  cdlemg39  36317  cdlemg40  36318  ltrncom  36339  tendotr  36431  cdlemk25-3  36505  cdlemk35s-id  36539  cdlemk39s-id  36541  cdlemk53b  36557  cdlemk53  36558  cdlemk55  36562  cdlemk35u  36565  cdlemk55u  36567  cdlemk39u  36569  cdlemk19u  36571  cdleml5N  36581  dia2dimlem7  36672  dia2dimlem13  36678  dih1dimatlem  36931  dihlsprn  36933  dihjat1lem  37030  dihjat1  37031  dvh2dim  37047  dochexmid  37070  lclkrlem1  37108  lclkrlem2i  37117  lclkrlem2t  37128  lcfrlem34  37178  lcfrlem38  37182  lcfrlem41  37185  mapdindp1  37322  mapdindp2  37323  mapdh6dN  37341  mapdh6jN  37347  mapdh8j  37390  mapdh8  37391  hdmap1l6d  37416  hdmap1l6j  37422  hdmap11lem2  37447  hdmap14lem7  37479