Theorem pm2.61dane 2730

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

Syntax hints:   -> wi 4   /\ wa 376   = wceq 1452   =/= wne 2641

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 190  df-an 378  df-ne 2643

This theorem is referenced by:  pm2.61da2ne  2731  pm2.61da3ne  2732  pm2.61iine  2733  disjxiun  4392  onfr  5469  f1oprswap  5868  soex  6755  riiner  7454  difsnen  7672  mapdom2  7761  nnunifi  7840  fofinf1o  7870  brwdom2  8106  cantnff  8197  cantnfp1  8204  carddomi2  8422  wdomfil  8510  fin1a2lem10  8857  fin1a2lem11  8858  uzsupss  11279  xaddcom  11555  xnegdi  11559  xpncan  11562  xleadd1a  11564  xsubge0  11572  cnpart  13380  fsumcllem  13875  fsumrev2  13920  expcnv  13999  geomulcvg  14009  fprodcllem  14082  fsumdvds  14425  gcd0id  14566  nn0seqcvgd  14608  lcmdvds  14652  mulgcddvds  14740  pcge0  14890  pcneg  14902  pcdvdstr  14904  pcz  14909  pcprmpw2  14910  pcadd  14913  ramcl2  15052  ramcl2OLD  15053  0ramcl  15060  ramub1lem1  15063  ramcl  15066  mrerintcl  15581  mreriincl  15582  mreexexlem4d  15631  mreclatBAD  16511  psgnunilem1  17212  odmulg  17285  sylow1lem1  17328  pgpfi  17335  odadd1  17564  odadd2  17565  gsumval3  17619  gsumpt  17672  dprdfcntz  17726  dprd2da  17753  ablfac1eulem  17783  pgpfaclem3  17794  abvneg  18140  lssssr  18254  lspsneq  18423  lspdisj2  18428  drngnidl  18530  cnsubrg  19105  riinopn  20015  riincld  20136  neipeltop  20222  hauscmplem  20498  cmpfi  20500  ptbasfi  20673  xkoccn  20711  txindislem  20725  txtube  20732  hmphindis  20889  fclscmp  21123  utop2nei  21343  nrginvrcn  21772  nmoleub  21814  nmoleubOLD  21830  blcvx  21894  xrsxmet  21905  xrsblre  21907  lebnumlem3  22069  lebnumlem3OLD  22072  cphsqrtcl2  22242  ovollb2  22520  ioorcl  22608  ioorclOLD  22613  i1fmulc  22740  itg1mulc  22741  mbfi1fseqlem4  22755  dvlip  23024  dvne0  23042  ig1pdvds  23207  ig1pdvdsOLD  23213  plyeq0lem  23243  plyeq0  23244  aannenlem2  23364  aalioulem6  23372  abelthlem8  23473  abelth  23475  cxpexp  23692  cxpge0  23707  cxpmul2  23713  abscxp2  23717  abscxpbnd  23772  cxpeq  23776  nnlogbexp  23797  isosctrlem2  23827  atanrecl  23916  wilthlem2  24073  dchrabs2  24269  dchr1re  24270  lgsneg1  24327  lgsdirprm  24336  lgsdir  24337  lgsne0  24340  lgsdirnn0  24346  lgsdinn0  24347  2sqlem9  24380  rpvmasumlem  24404  dchrvmasumiflem1  24418  dchrisum0flblem1  24425  rpvmasum2  24429  pntrsumbnd2  24484  pntleml  24528  tgcgrextend  24608  tgbtwnexch2  24619  tgifscgr  24632  tgcolg  24678  tgidinside  24695  tgbtwnconn1lem2  24697  tgbtwnconn1lem3  24698  lnhl  24739  tglinethru  24760  tglnpt2  24765  tglineneq  24768  coltr  24771  coltr3  24772  colline  24773  mirreu3  24778  miriso  24794  mirln  24800  mirln2  24801  mirconn  24802  mirbtwnhl  24804  colmid  24812  krippenlem  24814  midexlem  24816  ragflat  24828  ragcgr  24831  perprag  24847  perpdragALT  24848  colperpexlem1  24851  colperpexlem3  24853  midex  24858  opphllem1  24868  opphllem2  24869  opphllem5  24872  opphllem6  24873  hlpasch  24877  lmiisolem  24917  hypcgrlem1  24920  hypcgrlem2  24921  cgrg3col4  24963  umgraex  25129  eupath2lem3  25786  nmcoplbi  27762  nmophmi  27765  nmbdfnlbi  27783  disjdifprg  28262  imadifxp  28288  xlt2addrd  28413  ssnnssfz  28442  psgnfzto1stlem  28687  locfinref  28742  esumpr2  28962  unelldsys  29054  sigapildsyslem  29057  sigapildsys  29058  mbfmcst  29154  carsgsigalem  29220  carsgclctunlem3  29225  pmeasmono  29230  probun  29325  0rrv  29357  sgncl  29482  signsvtn0  29531  signstfvneq0  29533  btwnconn1lem11  30935  finxp00  31864  poimirlem14  32018  mblfinlem1  32041  mblfinlem2  32042  ismblfin  32045  itg2addnclem  32057  itgaddnclem2  32065  bddiblnc  32076  areacirclem4  32099  areacirc  32101  isbnd3  32180  blbnd  32183  rrnequiv  32231  lsmsat  32645  lkrscss  32735  eqlkr  32736  lkrshpor  32744  atcvrj2b  33068  atltcvr  33071  3dim1  33103  3dim2  33104  3dim3  33105  ps-2  33114  2at0mat0  33161  dalemdnee  33302  dalem63  33371  lnatexN  33415  2llnma3r  33424  pmodlem1  33482  pmapjat1  33489  pclfinclN  33586  osumclN  33603  pexmidALTN  33614  lhpexle2lem  33645  lhpexle3lem  33647  4atexlemex6  33710  4atex  33712  trlnle  33823  trlval3  33824  cdlemc  33834  cdlemd9  33843  cdleme27N  34007  cdleme28c  34010  cdleme32fvaw  34077  cdleme42ke  34123  cdleme42keg  34124  cdleme42mgN  34126  cdleme17d  34136  cdleme48fvg  34138  cdleme50trn123  34192  cdlemb3  34244  cdlemg8  34269  cdlemg15a  34293  cdlemg15  34294  cdlemg16  34295  cdlemg16ALTN  34296  cdlemg16z  34297  cdlemg16zz  34298  cdlemg20  34323  cdlemg22  34325  cdlemg37  34327  cdlemg31d  34338  cdlemg39  34354  cdlemg40  34355  ltrncom  34376  tendotr  34468  cdlemk25-3  34542  cdlemk35s-id  34576  cdlemk39s-id  34578  cdlemk53b  34594  cdlemk53  34595  cdlemk55  34599  cdlemk35u  34602  cdlemk55u  34604  cdlemk39u  34606  cdlemk19u  34608  cdleml5N  34618  dia2dimlem7  34709  dia2dimlem13  34715  dih1dimatlem  34968  dihlsprn  34970  dihjat1lem  35067  dihjat1  35068  dvh2dim  35084  dochexmid  35107  lclkrlem1  35145  lclkrlem2i  35154  lclkrlem2t  35165  lcfrlem34  35215  lcfrlem38  35219  lcfrlem41  35222  mapdindp1  35359  mapdindp2  35360  mapdh6dN  35378  mapdh6jN  35384  mapdh8j  35427  mapdh8  35428  hdmap1l6d  35453  hdmap1l6j  35459  hdmap11lem2  35484  hdmap14lem7  35516  jm2.19  35919  jm2.23  35922  nzss  36736  stoweidlem58  38031  fourierdlem41  38123  fourierdlem48  38130  fouriersw  38207  etransclem24  38235  upgrex  39338  crctcsh1wlk  40000  crctcsh  40002  11wlkdlem2  40026  eupth2lem3lem3  40142  eupth2lem3lem7  40146  ssnn0ssfz  40638