MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.61dane Unicode version

Theorem pm2.61dane 2599
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
StepHypRef Expression
1 pm2.61dane.1 . . 3  |-  ( (
ph  /\  A  =  B )  ->  ps )
21ex 423 . 2  |-  ( ph  ->  ( A  =  B  ->  ps ) )
3 pm2.61dane.2 . . 3  |-  ( (
ph  /\  A  =/=  B )  ->  ps )
43ex 423 . 2  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )
52, 4pm2.61dne 2598 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1642    =/= wne 2521
This theorem is referenced by:  pm2.61da2ne  2600  pm2.61da3ne  2601  disjxiun  4101  onfr  4513  soex  5204  f1oprswap  5598  riiner  6819  difsnen  7032  mapdom2  7120  nnunifi  7198  fofinf1o  7227  brwdom2  7377  cantnff  7465  cantnfp1  7473  carddomi2  7693  wdomfil  7778  fin1a2lem10  8125  fin1a2lem11  8126  uzsupss  10402  xaddcom  10657  xnegdi  10660  xpncan  10663  xleadd1a  10665  xsubge0  10673  cnpart  11821  fsumcllem  12302  fsumrev2  12341  expcnv  12419  geomulcvg  12429  fsumdvds  12669  gcd0id  12799  nn0seqcvgd  12837  mulgcddvds  12880  pcge0  13011  pcneg  13023  pcdvdstr  13025  pcz  13030  pcprmpw2  13031  pcadd  13034  ramcl2  13160  0ramcl  13167  ramub1lem1  13170  ramcl  13173  mrerintcl  13598  mreriincl  13599  mreexexlem4d  13648  mreclat  14389  odmulg  14968  sylow1lem1  15008  pgpfi  15015  odadd1  15239  odadd2  15240  gsumval3  15290  gsumpt  15321  dprdfcntz  15349  dprd2da  15376  ablfac1eulem  15406  pgpfaclem3  15417  abvneg  15698  lssssr  15809  lspsneq  15974  lspdisj2  15979  drngnidl  16080  cnsubrg  16538  riinopn  16760  riincld  16887  hauscmplem  17239  cmpfi  17241  ptbasfi  17382  xkoccn  17419  txindislem  17433  txtube  17440  hmphindis  17594  fclscmp  17827  nrginvrcn  18304  nmoleub  18342  blcvx  18406  xrsxmet  18417  xrsblre  18419  lebnumlem3  18565  cphsqrcl2  18726  ovollb2  18952  ioorcl  19036  i1fmulc  19162  itg1mulc  19163  mbfi1fseqlem4  19177  dvlip  19444  dvne0  19462  ig1pdvds  19666  plyeq0lem  19696  plyeq0  19697  aannenlem2  19813  aalioulem6  19821  abelthlem8  19922  abelth  19924  cxpexp  20126  cxpge0  20141  cxpmul2  20147  abscxp2  20151  abscxpbnd  20204  cxpeq  20208  isosctrlem2  20230  atanrecl  20318  wilthlem2  20419  dchrabs2  20613  dchr1re  20614  lgsneg1  20671  lgsdirprm  20680  lgsdir  20681  lgsne0  20684  lgsdirnn0  20690  lgsdinn0  20691  2sqlem9  20724  rpvmasumlem  20748  dchrvmasumiflem1  20762  dchrisum0flblem1  20769  rpvmasum2  20773  pntrsumbnd2  20828  pntleml  20872  nmcoplbi  22722  nmophmi  22725  nmbdfnlbi  22743  disjdifprg  23216  imadifxp  23241  xlt2addrd  23325  neipeltop  23442  esumpr2  23724  mbfmcst  23873  probun  23926  0rrv  23958  umgraex  24279  eupath2lem3  24307  fprodcllem  24578  btwnconn1lem11  25279  itg2addnclem  25492  itg2addnc  25494  bddiblnc  25510  areacirclem5  25521  areacirc  25523  isbnd3  25831  blbnd  25834  rrnequiv  25882  jm2.19  26409  jm2.23  26412  psgnunilem1  26739  lsmsat  29267  lkrscss  29357  eqlkr  29358  lkrshpor  29366  atcvrj2b  29690  atltcvr  29693  3dim1  29725  3dim2  29726  3dim3  29727  ps-2  29736  2at0mat0  29783  dalemdnee  29924  dalem63  29993  lnatexN  30037  2llnma3r  30046  pmodlem1  30104  pmapjat1  30111  pclfinclN  30208  osumclN  30225  pexmidALTN  30236  lhpexle2lem  30267  lhpexle3lem  30269  4atexlemex6  30332  4atex  30334  trlnle  30444  trlval3  30445  cdlemc  30455  cdlemd9  30464  cdleme27N  30627  cdleme28c  30630  cdleme32fvaw  30697  cdleme42ke  30743  cdleme42keg  30744  cdleme42mgN  30746  cdleme17d  30756  cdleme48fvg  30758  cdleme50trn123  30812  cdlemb3  30864  cdlemg8  30889  cdlemg15a  30913  cdlemg15  30914  cdlemg16  30915  cdlemg16ALTN  30916  cdlemg16z  30917  cdlemg16zz  30918  cdlemg20  30943  cdlemg22  30945  cdlemg37  30947  cdlemg31d  30958  cdlemg39  30974  cdlemg40  30975  ltrncom  30996  tendotr  31088  cdlemk25-3  31162  cdlemk35s-id  31196  cdlemk39s-id  31198  cdlemk53b  31214  cdlemk53  31215  cdlemk55  31219  cdlemk35u  31222  cdlemk55u  31224  cdlemk39u  31226  cdlemk19u  31228  cdleml5N  31238  dia2dimlem7  31329  dia2dimlem13  31335  dih1dimatlem  31588  dihlsprn  31590  dihjat1lem  31687  dihjat1  31688  dvh2dim  31704  dochexmid  31727  lclkrlem1  31765  lclkrlem2i  31774  lclkrlem2t  31785  lcfrlem34  31835  lcfrlem38  31839  lcfrlem41  31842  mapdindp1  31979  mapdindp2  31980  mapdh6dN  31998  mapdh6jN  32004  mapdh8j  32047  mapdh8  32048  hdmap1l6d  32073  hdmap1l6j  32079  hdmap11lem2  32104  hdmap14lem7  32136
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 177  df-an 360  df-ne 2523
  Copyright terms: Public domain W3C validator