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

Theorem pm2.61dane 2910
Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.)
Hypotheses
Ref Expression
pm2.61dane.1 ((𝜑𝐴 = 𝐵) → 𝜓)
pm2.61dane.2 ((𝜑𝐴𝐵) → 𝜓)
Assertion
Ref Expression
pm2.61dane (𝜑𝜓)

Proof of Theorem pm2.61dane
StepHypRef Expression
1 pm2.61dane.1 . . 3 ((𝜑𝐴 = 𝐵) → 𝜓)
21ex 449 . 2 (𝜑 → (𝐴 = 𝐵𝜓))
3 pm2.61dane.2 . . 3 ((𝜑𝐴𝐵) → 𝜓)
43ex 449 . 2 (𝜑 → (𝐴𝐵𝜓))
52, 4pm2.61dne 2909 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wne 2823
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 197  df-an 385  df-ne 2824
This theorem is referenced by:  pm2.61da2ne  2911  pm2.61da3ne  2912  pm2.61iine  2913  disjxiun  4681  disjxiunOLD  4682  onfr  5801  f1oprswap  6218  soex  7151  riiner  7863  difsnen  8083  mapdom2  8172  nnunifi  8252  fofinf1o  8282  brwdom2  8519  cantnff  8609  cantnfp1  8616  carddomi2  8834  wdomfil  8922  fin1a2lem10  9269  fin1a2lem11  9270  uzsupss  11818  xaddcom  12109  xnegdi  12116  xpncan  12119  xleadd1a  12121  xsubge0  12129  cnpart  14024  fsumcllem  14507  fsumrev2  14558  expcnv  14640  geomulcvg  14651  fprodcllem  14725  fsumdvds  15077  gcd0id  15287  nn0seqcvgd  15330  lcmdvds  15368  mulgcddvds  15416  pcge0  15613  pcneg  15625  pcdvdstr  15627  pcz  15632  pcprmpw2  15633  pcadd  15640  ramcl2  15767  0ramcl  15774  ramub1lem1  15777  ramcl  15780  mrerintcl  16304  mreriincl  16305  mreexexlem4d  16354  mreclatBAD  17234  psgnunilem1  17959  odmulg  18019  sylow1lem1  18059  pgpfi  18066  odadd1  18297  odadd2  18298  gsumval3  18354  gsumpt  18407  dprdfcntz  18460  dprd2da  18487  ablfac1eulem  18517  pgpfaclem3  18528  abvneg  18882  lssssr  19001  lspsneq  19170  lspdisj2  19175  drngnidl  19277  cnsubrg  19854  riinopn  20761  riincld  20896  neipeltop  20981  hauscmplem  21257  cmpfi  21259  ptbasfi  21432  xkoccn  21470  txindislem  21484  txtube  21491  hmphindis  21648  fclscmp  21881  utop2nei  22101  nrginvrcn  22543  nmoleub  22582  blcvx  22648  xrsxmet  22659  xrsblre  22661  lebnumlem3  22809  cphsqrtcl2  23032  ovollb2  23303  ioorcl  23391  i1fmulc  23515  itg1mulc  23516  mbfi1fseqlem4  23530  dvlip  23801  dvne0  23819  ig1pdvds  23981  plyeq0lem  24011  plyeq0  24012  aannenlem2  24129  aalioulem6  24137  abelthlem8  24238  abelth  24240  cxpexp  24459  cxpge0  24474  cxpmul2  24480  abscxp2  24484  abscxpbnd  24539  cxpeq  24543  nnlogbexp  24564  isosctrlem2  24594  atanrecl  24683  wilthlem2  24840  dchrabs2  25032  dchr1re  25033  lgsneg1  25092  lgsdirprm  25101  lgsdir  25102  lgsne0  25105  lgsdirnn0  25114  lgsdinn0  25115  2sqlem9  25197  rpvmasumlem  25221  dchrvmasumiflem1  25235  dchrisum0flblem1  25242  rpvmasum2  25246  pntrsumbnd2  25301  pntleml  25345  tgcgrextend  25425  tgbtwnexch2  25436  tgifscgr  25448  tgcolg  25494  tgidinside  25511  tgbtwnconn1lem2  25513  tgbtwnconn1lem3  25514  lnhl  25555  tglinethru  25576  tglnpt2  25581  tglineneq  25584  coltr  25587  coltr3  25588  colline  25589  mirreu3  25594  miriso  25610  mirln  25616  mirln2  25617  mirconn  25618  mirbtwnhl  25620  colmid  25628  krippenlem  25630  midexlem  25632  ragflat  25644  ragcgr  25647  perprag  25663  perpdragALT  25664  colperpexlem1  25667  colperpexlem3  25669  midex  25674  opphllem1  25684  opphllem2  25685  opphllem5  25688  opphllem6  25689  hlpasch  25693  lmiisolem  25733  hypcgrlem1  25736  hypcgrlem2  25737  cgrg3col4  25779  upgrex  26032  crctcshwlk  26770  crctcsh  26772  1wlkdlem2  27116  eupth2lem3lem3  27208  eupth2lem3lem7  27212  nmcoplbi  29015  nmophmi  29018  nmbdfnlbi  29036  disjdifprg  29514  imadifxp  29540  xlt2addrd  29651  ssnnssfz  29677  psgnfzto1stlem  29978  pmtridf1o  29984  pmtridfv1  29985  pmtridfv2  29986  locfinref  30036  esumpr2  30257  unelldsys  30349  sigapildsyslem  30352  sigapildsys  30353  mbfmcst  30449  carsgsigalem  30505  carsgclctunlem3  30510  pmeasmono  30514  probun  30609  0rrv  30641  sgncl  30728  signsvtn0  30775  signstfvneq0  30777  btwnconn1lem11  32329  finxp00  33369  matunitlindf  33537  poimirlem14  33553  mblfinlem1  33576  mblfinlem2  33577  ismblfin  33580  itg2addnclem  33591  itgaddnclem2  33599  bddiblnc  33610  areacirclem4  33633  areacirc  33635  isbnd3  33713  blbnd  33716  rrnequiv  33764  lsmsat  34613  lkrscss  34703  eqlkr  34704  lkrshpor  34712  atcvrj2b  35036  atltcvr  35039  3dim1  35071  3dim2  35072  3dim3  35073  ps-2  35082  2at0mat0  35129  dalemdnee  35270  dalem63  35339  lnatexN  35383  2llnma3r  35392  pmodlem1  35450  pmapjat1  35457  pclfinclN  35554  osumclN  35571  pexmidALTN  35582  lhpexle2lem  35613  lhpexle3lem  35615  4atexlemex6  35678  4atex  35680  trlnle  35791  trlval3  35792  cdlemc  35802  cdlemd9  35811  cdleme27N  35974  cdleme28c  35977  cdleme32fvaw  36044  cdleme42ke  36090  cdleme42keg  36091  cdleme42mgN  36093  cdleme17d  36103  cdleme48fvg  36105  cdleme50trn123  36159  cdlemb3  36211  cdlemg8  36236  cdlemg15a  36260  cdlemg15  36261  cdlemg16  36262  cdlemg16ALTN  36263  cdlemg16z  36264  cdlemg16zz  36265  cdlemg20  36290  cdlemg22  36292  cdlemg37  36294  cdlemg31d  36305  cdlemg39  36321  cdlemg40  36322  ltrncom  36343  tendotr  36435  cdlemk25-3  36509  cdlemk35s-id  36543  cdlemk39s-id  36545  cdlemk53b  36561  cdlemk53  36562  cdlemk55  36566  cdlemk35u  36569  cdlemk55u  36571  cdlemk39u  36573  cdlemk19u  36575  cdleml5N  36585  dia2dimlem7  36676  dia2dimlem13  36682  dih1dimatlem  36935  dihlsprn  36937  dihjat1lem  37034  dihjat1  37035  dvh2dim  37051  dochexmid  37074  lclkrlem1  37112  lclkrlem2i  37121  lclkrlem2t  37132  lcfrlem34  37182  lcfrlem38  37186  lcfrlem41  37189  mapdindp1  37326  mapdindp2  37327  mapdh6dN  37345  mapdh6jN  37351  mapdh8j  37394  mapdh8  37395  hdmap1l6d  37420  hdmap1l6j  37426  hdmap11lem2  37451  hdmap14lem7  37483  jm2.19  37877  jm2.23  37880  nzss  38833  cnrefiisplem  40373  stoweidlem58  40593  fourierdlem41  40683  fourierdlem48  40689  fouriersw  40766  etransclem24  40793  nnfoctbdjlem  40990  ssnn0ssfz  42452
  Copyright terms: Public domain W3C validator