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

Theorem pm2.61dane 2649
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 2648 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    =/= wne 2571
This theorem is referenced by:  pm2.61da2ne  2650  pm2.61da3ne  2651  disjxiun  4173  onfr  4584  soex  5282  f1oprswap  5680  riiner  6940  difsnen  7153  mapdom2  7241  nnunifi  7321  fofinf1o  7350  brwdom2  7501  cantnff  7589  cantnfp1  7597  carddomi2  7817  wdomfil  7902  fin1a2lem10  8249  fin1a2lem11  8250  uzsupss  10528  xaddcom  10784  xnegdi  10787  xpncan  10790  xleadd1a  10792  xsubge0  10800  cnpart  12004  fsumcllem  12485  fsumrev2  12524  expcnv  12602  geomulcvg  12612  fsumdvds  12852  gcd0id  12982  nn0seqcvgd  13020  mulgcddvds  13063  pcge0  13194  pcneg  13206  pcdvdstr  13208  pcz  13213  pcprmpw2  13214  pcadd  13217  ramcl2  13343  0ramcl  13350  ramub1lem1  13353  ramcl  13356  mrerintcl  13781  mreriincl  13782  mreexexlem4d  13831  mreclat  14572  odmulg  15151  sylow1lem1  15191  pgpfi  15198  odadd1  15422  odadd2  15423  gsumval3  15473  gsumpt  15504  dprdfcntz  15532  dprd2da  15559  ablfac1eulem  15589  pgpfaclem3  15600  abvneg  15881  lssssr  15988  lspsneq  16153  lspdisj2  16158  drngnidl  16259  cnsubrg  16718  riinopn  16940  riincld  17067  neipeltop  17152  hauscmplem  17427  cmpfi  17429  ptbasfi  17570  xkoccn  17608  txindislem  17622  txtube  17629  hmphindis  17786  fclscmp  18019  utop2nei  18237  nrginvrcn  18684  nmoleub  18722  blcvx  18786  xrsxmet  18797  xrsblre  18799  lebnumlem3  18945  cphsqrcl2  19106  ovollb2  19342  ioorcl  19426  i1fmulc  19552  itg1mulc  19553  mbfi1fseqlem4  19567  dvlip  19834  dvne0  19852  ig1pdvds  20056  plyeq0lem  20086  plyeq0  20087  aannenlem2  20203  aalioulem6  20211  abelthlem8  20312  abelth  20314  cxpexp  20516  cxpge0  20531  cxpmul2  20537  abscxp2  20541  abscxpbnd  20594  cxpeq  20598  isosctrlem2  20620  atanrecl  20708  wilthlem2  20809  dchrabs2  21003  dchr1re  21004  lgsneg1  21061  lgsdirprm  21070  lgsdir  21071  lgsne0  21074  lgsdirnn0  21080  lgsdinn0  21081  2sqlem9  21114  rpvmasumlem  21138  dchrvmasumiflem1  21152  dchrisum0flblem1  21159  rpvmasum2  21163  pntrsumbnd2  21218  pntleml  21262  umgraex  21315  eupath2lem3  21658  nmcoplbi  23488  nmophmi  23491  nmbdfnlbi  23509  disjdifprg  23974  imadifxp  23995  xlt2addrd  24081  ssnnssfz  24105  nnlogbexp  24361  esumpr2  24415  mbfmcst  24566  probun  24634  0rrv  24666  fprodcllem  25234  btwnconn1lem11  25939  mblfinlem  26147  ismblfin  26150  itg2addnclem  26159  itgaddnclem2  26167  bddiblnc  26178  areacirclem5  26189  areacirc  26191  isbnd3  26387  blbnd  26390  rrnequiv  26438  jm2.19  26958  jm2.23  26961  psgnunilem1  27288  stoweidlem58  27678  lsmsat  29495  lkrscss  29585  eqlkr  29586  lkrshpor  29594  atcvrj2b  29918  atltcvr  29921  3dim1  29953  3dim2  29954  3dim3  29955  ps-2  29964  2at0mat0  30011  dalemdnee  30152  dalem63  30221  lnatexN  30265  2llnma3r  30274  pmodlem1  30332  pmapjat1  30339  pclfinclN  30436  osumclN  30453  pexmidALTN  30464  lhpexle2lem  30495  lhpexle3lem  30497  4atexlemex6  30560  4atex  30562  trlnle  30672  trlval3  30673  cdlemc  30683  cdlemd9  30692  cdleme27N  30855  cdleme28c  30858  cdleme32fvaw  30925  cdleme42ke  30971  cdleme42keg  30972  cdleme42mgN  30974  cdleme17d  30984  cdleme48fvg  30986  cdleme50trn123  31040  cdlemb3  31092  cdlemg8  31117  cdlemg15a  31141  cdlemg15  31142  cdlemg16  31143  cdlemg16ALTN  31144  cdlemg16z  31145  cdlemg16zz  31146  cdlemg20  31171  cdlemg22  31173  cdlemg37  31175  cdlemg31d  31186  cdlemg39  31202  cdlemg40  31203  ltrncom  31224  tendotr  31316  cdlemk25-3  31390  cdlemk35s-id  31424  cdlemk39s-id  31426  cdlemk53b  31442  cdlemk53  31443  cdlemk55  31447  cdlemk35u  31450  cdlemk55u  31452  cdlemk39u  31454  cdlemk19u  31456  cdleml5N  31466  dia2dimlem7  31557  dia2dimlem13  31563  dih1dimatlem  31816  dihlsprn  31818  dihjat1lem  31915  dihjat1  31916  dvh2dim  31932  dochexmid  31955  lclkrlem1  31993  lclkrlem2i  32002  lclkrlem2t  32013  lcfrlem34  32063  lcfrlem38  32067  lcfrlem41  32070  mapdindp1  32207  mapdindp2  32208  mapdh6dN  32226  mapdh6jN  32232  mapdh8j  32275  mapdh8  32276  hdmap1l6d  32301  hdmap1l6j  32307  hdmap11lem2  32332  hdmap14lem7  32364
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 2573
  Copyright terms: Public domain W3C validator