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

Theorem pm2.61dane 2682
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 424 . 2  |-  ( ph  ->  ( A  =  B  ->  ps ) )
3 pm2.61dane.2 . . 3  |-  ( (
ph  /\  A  =/=  B )  ->  ps )
43ex 424 . 2  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )
52, 4pm2.61dne 2681 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    =/= wne 2599
This theorem is referenced by:  pm2.61da2ne  2683  pm2.61da3ne  2684  disjxiun  4209  onfr  4620  soex  5319  f1oprswap  5717  riiner  6977  difsnen  7190  mapdom2  7278  nnunifi  7358  fofinf1o  7387  brwdom2  7541  cantnff  7629  cantnfp1  7637  carddomi2  7857  wdomfil  7942  fin1a2lem10  8289  fin1a2lem11  8290  uzsupss  10568  xaddcom  10824  xnegdi  10827  xpncan  10830  xleadd1a  10832  xsubge0  10840  cnpart  12045  fsumcllem  12526  fsumrev2  12565  expcnv  12643  geomulcvg  12653  fsumdvds  12893  gcd0id  13023  nn0seqcvgd  13061  mulgcddvds  13104  pcge0  13235  pcneg  13247  pcdvdstr  13249  pcz  13254  pcprmpw2  13255  pcadd  13258  ramcl2  13384  0ramcl  13391  ramub1lem1  13394  ramcl  13397  mrerintcl  13822  mreriincl  13823  mreexexlem4d  13872  mreclat  14613  odmulg  15192  sylow1lem1  15232  pgpfi  15239  odadd1  15463  odadd2  15464  gsumval3  15514  gsumpt  15545  dprdfcntz  15573  dprd2da  15600  ablfac1eulem  15630  pgpfaclem3  15641  abvneg  15922  lssssr  16029  lspsneq  16194  lspdisj2  16199  drngnidl  16300  cnsubrg  16759  riinopn  16981  riincld  17108  neipeltop  17193  hauscmplem  17469  cmpfi  17471  ptbasfi  17613  xkoccn  17651  txindislem  17665  txtube  17672  hmphindis  17829  fclscmp  18062  utop2nei  18280  nrginvrcn  18727  nmoleub  18765  blcvx  18829  xrsxmet  18840  xrsblre  18842  lebnumlem3  18988  cphsqrcl2  19149  ovollb2  19385  ioorcl  19469  i1fmulc  19595  itg1mulc  19596  mbfi1fseqlem4  19610  dvlip  19877  dvne0  19895  ig1pdvds  20099  plyeq0lem  20129  plyeq0  20130  aannenlem2  20246  aalioulem6  20254  abelthlem8  20355  abelth  20357  cxpexp  20559  cxpge0  20574  cxpmul2  20580  abscxp2  20584  abscxpbnd  20637  cxpeq  20641  isosctrlem2  20663  atanrecl  20751  wilthlem2  20852  dchrabs2  21046  dchr1re  21047  lgsneg1  21104  lgsdirprm  21113  lgsdir  21114  lgsne0  21117  lgsdirnn0  21123  lgsdinn0  21124  2sqlem9  21157  rpvmasumlem  21181  dchrvmasumiflem1  21195  dchrisum0flblem1  21202  rpvmasum2  21206  pntrsumbnd2  21261  pntleml  21305  umgraex  21358  eupath2lem3  21701  nmcoplbi  23531  nmophmi  23534  nmbdfnlbi  23552  disjdifprg  24017  imadifxp  24038  xlt2addrd  24124  ssnnssfz  24148  nnlogbexp  24404  esumpr2  24458  mbfmcst  24609  probun  24677  0rrv  24709  fprodcllem  25277  btwnconn1lem11  26031  mblfinlem1  26243  mblfinlem2  26244  ismblfin  26247  itg2addnclem  26256  itgaddnclem2  26264  bddiblnc  26275  areacirclem4  26295  areacirc  26297  isbnd3  26493  blbnd  26496  rrnequiv  26544  jm2.19  27064  jm2.23  27067  psgnunilem1  27393  stoweidlem58  27783  lsmsat  29806  lkrscss  29896  eqlkr  29897  lkrshpor  29905  atcvrj2b  30229  atltcvr  30232  3dim1  30264  3dim2  30265  3dim3  30266  ps-2  30275  2at0mat0  30322  dalemdnee  30463  dalem63  30532  lnatexN  30576  2llnma3r  30585  pmodlem1  30643  pmapjat1  30650  pclfinclN  30747  osumclN  30764  pexmidALTN  30775  lhpexle2lem  30806  lhpexle3lem  30808  4atexlemex6  30871  4atex  30873  trlnle  30983  trlval3  30984  cdlemc  30994  cdlemd9  31003  cdleme27N  31166  cdleme28c  31169  cdleme32fvaw  31236  cdleme42ke  31282  cdleme42keg  31283  cdleme42mgN  31285  cdleme17d  31295  cdleme48fvg  31297  cdleme50trn123  31351  cdlemb3  31403  cdlemg8  31428  cdlemg15a  31452  cdlemg15  31453  cdlemg16  31454  cdlemg16ALTN  31455  cdlemg16z  31456  cdlemg16zz  31457  cdlemg20  31482  cdlemg22  31484  cdlemg37  31486  cdlemg31d  31497  cdlemg39  31513  cdlemg40  31514  ltrncom  31535  tendotr  31627  cdlemk25-3  31701  cdlemk35s-id  31735  cdlemk39s-id  31737  cdlemk53b  31753  cdlemk53  31754  cdlemk55  31758  cdlemk35u  31761  cdlemk55u  31763  cdlemk39u  31765  cdlemk19u  31767  cdleml5N  31777  dia2dimlem7  31868  dia2dimlem13  31874  dih1dimatlem  32127  dihlsprn  32129  dihjat1lem  32226  dihjat1  32227  dvh2dim  32243  dochexmid  32266  lclkrlem1  32304  lclkrlem2i  32313  lclkrlem2t  32324  lcfrlem34  32374  lcfrlem38  32378  lcfrlem41  32381  mapdindp1  32518  mapdindp2  32519  mapdh6dN  32537  mapdh6jN  32543  mapdh8j  32586  mapdh8  32587  hdmap1l6d  32612  hdmap1l6j  32618  hdmap11lem2  32643  hdmap14lem7  32675
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 2601
  Copyright terms: Public domain W3C validator