Theorem pm2.61dane 2645

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

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1649   =/= wne 2567

This theorem is referenced by:  pm2.61da2ne  2646  pm2.61da3ne  2647  disjxiun  4169  onfr  4580  soex  5278  f1oprswap  5676  riiner  6936  difsnen  7149  mapdom2  7237  nnunifi  7317  fofinf1o  7346  brwdom2  7497  cantnff  7585  cantnfp1  7593  carddomi2  7813  wdomfil  7898  fin1a2lem10  8245  fin1a2lem11  8246  uzsupss  10524  xaddcom  10780  xnegdi  10783  xpncan  10786  xleadd1a  10788  xsubge0  10796  cnpart  12000  fsumcllem  12481  fsumrev2  12520  expcnv  12598  geomulcvg  12608  fsumdvds  12848  gcd0id  12978  nn0seqcvgd  13016  mulgcddvds  13059  pcge0  13190  pcneg  13202  pcdvdstr  13204  pcz  13209  pcprmpw2  13210  pcadd  13213  ramcl2  13339  0ramcl  13346  ramub1lem1  13349  ramcl  13352  mrerintcl  13777  mreriincl  13778  mreexexlem4d  13827  mreclat  14568  odmulg  15147  sylow1lem1  15187  pgpfi  15194  odadd1  15418  odadd2  15419  gsumval3  15469  gsumpt  15500  dprdfcntz  15528  dprd2da  15555  ablfac1eulem  15585  pgpfaclem3  15596  abvneg  15877  lssssr  15984  lspsneq  16149  lspdisj2  16154  drngnidl  16255  cnsubrg  16714  riinopn  16936  riincld  17063  neipeltop  17148  hauscmplem  17423  cmpfi  17425  ptbasfi  17566  xkoccn  17604  txindislem  17618  txtube  17625  hmphindis  17782  fclscmp  18015  utop2nei  18233  nrginvrcn  18680  nmoleub  18718  blcvx  18782  xrsxmet  18793  xrsblre  18795  lebnumlem3  18941  cphsqrcl2  19102  ovollb2  19338  ioorcl  19422  i1fmulc  19548  itg1mulc  19549  mbfi1fseqlem4  19563  dvlip  19830  dvne0  19848  ig1pdvds  20052  plyeq0lem  20082  plyeq0  20083  aannenlem2  20199  aalioulem6  20207  abelthlem8  20308  abelth  20310  cxpexp  20512  cxpge0  20527  cxpmul2  20533  abscxp2  20537  abscxpbnd  20590  cxpeq  20594  isosctrlem2  20616  atanrecl  20704  wilthlem2  20805  dchrabs2  20999  dchr1re  21000  lgsneg1  21057  lgsdirprm  21066  lgsdir  21067  lgsne0  21070  lgsdirnn0  21076  lgsdinn0  21077  2sqlem9  21110  rpvmasumlem  21134  dchrvmasumiflem1  21148  dchrisum0flblem1  21155  rpvmasum2  21159  pntrsumbnd2  21214  pntleml  21258  umgraex  21311  eupath2lem3  21654  nmcoplbi  23484  nmophmi  23487  nmbdfnlbi  23505  disjdifprg  23970  imadifxp  23991  xlt2addrd  24077  ssnnssfz  24101  nnlogbexp  24357  esumpr2  24411  mbfmcst  24562  probun  24630  0rrv  24662  fprodcllem  25230  btwnconn1lem11  25935  mblfinlem  26143  ismblfin  26146  itg2addnclem  26155  itgaddnclem2  26163  bddiblnc  26174  areacirclem5  26185  areacirc  26187  isbnd3  26383  blbnd  26386  rrnequiv  26434  jm2.19  26954  jm2.23  26957  psgnunilem1  27284  stoweidlem58  27674  lsmsat  29491  lkrscss  29581  eqlkr  29582  lkrshpor  29590  atcvrj2b  29914  atltcvr  29917  3dim1  29949  3dim2  29950  3dim3  29951  ps-2  29960  2at0mat0  30007  dalemdnee  30148  dalem63  30217  lnatexN  30261  2llnma3r  30270  pmodlem1  30328  pmapjat1  30335  pclfinclN  30432  osumclN  30449  pexmidALTN  30460  lhpexle2lem  30491  lhpexle3lem  30493  4atexlemex6  30556  4atex  30558  trlnle  30668  trlval3  30669  cdlemc  30679  cdlemd9  30688  cdleme27N  30851  cdleme28c  30854  cdleme32fvaw  30921  cdleme42ke  30967  cdleme42keg  30968  cdleme42mgN  30970  cdleme17d  30980  cdleme48fvg  30982  cdleme50trn123  31036  cdlemb3  31088  cdlemg8  31113  cdlemg15a  31137  cdlemg15  31138  cdlemg16  31139  cdlemg16ALTN  31140  cdlemg16z  31141  cdlemg16zz  31142  cdlemg20  31167  cdlemg22  31169  cdlemg37  31171  cdlemg31d  31182  cdlemg39  31198  cdlemg40  31199  ltrncom  31220  tendotr  31312  cdlemk25-3  31386  cdlemk35s-id  31420  cdlemk39s-id  31422  cdlemk53b  31438  cdlemk53  31439  cdlemk55  31443  cdlemk35u  31446  cdlemk55u  31448  cdlemk39u  31450  cdlemk19u  31452  cdleml5N  31462  dia2dimlem7  31553  dia2dimlem13  31559  dih1dimatlem  31812  dihlsprn  31814  dihjat1lem  31911  dihjat1  31912  dvh2dim  31928  dochexmid  31951  lclkrlem1  31989  lclkrlem2i  31998  lclkrlem2t  32009  lcfrlem34  32059  lcfrlem38  32063  lcfrlem41  32066  mapdindp1  32203  mapdindp2  32204  mapdh6dN  32222  mapdh6jN  32228  mapdh8j  32271  mapdh8  32272  hdmap1l6d  32297  hdmap1l6j  32303  hdmap11lem2  32328  hdmap14lem7  32360

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-ne 2569