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 3019
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 3018 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1632  wne 2932
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 2933
This theorem is referenced by:  pm2.61da2ne  3020  pm2.61da3ne  3021  pm2.61iine  3022  disjxiun  4801  onfr  5924  f1oprswap  6341  soex  7274  riiner  7987  difsnen  8207  mapdom2  8296  nnunifi  8376  fofinf1o  8406  brwdom2  8643  cantnff  8744  cantnfp1  8751  carddomi2  8986  wdomfil  9074  fin1a2lem10  9423  fin1a2lem11  9424  uzsupss  11973  xaddcom  12264  xnegdi  12271  xpncan  12274  xleadd1a  12276  xsubge0  12284  cnpart  14179  fsumcllem  14662  fsumrev2  14713  expcnv  14795  geomulcvg  14806  fprodcllem  14880  fsumdvds  15232  gcd0id  15442  nn0seqcvgd  15485  lcmdvds  15523  mulgcddvds  15571  pcge0  15768  pcneg  15780  pcdvdstr  15782  pcz  15787  pcprmpw2  15788  pcadd  15795  ramcl2  15922  0ramcl  15929  ramub1lem1  15932  ramcl  15935  mrerintcl  16459  mreriincl  16460  mreexexlem4d  16509  mreclatBAD  17388  psgnunilem1  18113  odmulg  18173  sylow1lem1  18213  pgpfi  18220  odadd1  18451  odadd2  18452  gsumval3  18508  gsumpt  18561  dprdfcntz  18614  dprd2da  18641  ablfac1eulem  18671  pgpfaclem3  18682  abvneg  19036  lssssr  19155  lspsneq  19324  lspdisj2  19329  drngnidl  19431  cnsubrg  20008  riinopn  20915  riincld  21050  neipeltop  21135  hauscmplem  21411  cmpfi  21413  ptbasfi  21586  xkoccn  21624  txindislem  21638  txtube  21645  hmphindis  21802  fclscmp  22035  utop2nei  22255  nrginvrcn  22697  nmoleub  22736  blcvx  22802  xrsxmet  22813  xrsblre  22815  lebnumlem3  22963  cphsqrtcl2  23186  ovollb2  23457  ioorcl  23545  i1fmulc  23669  itg1mulc  23670  mbfi1fseqlem4  23684  dvlip  23955  dvne0  23973  ig1pdvds  24135  plyeq0lem  24165  plyeq0  24166  aannenlem2  24283  aalioulem6  24291  abelthlem8  24392  abelth  24394  cxpexp  24613  cxpge0  24628  cxpmul2  24634  abscxp2  24638  abscxpbnd  24693  cxpeq  24697  nnlogbexp  24718  isosctrlem2  24748  atanrecl  24837  wilthlem2  24994  dchrabs2  25186  dchr1re  25187  lgsneg1  25246  lgsdirprm  25255  lgsdir  25256  lgsne0  25259  lgsdirnn0  25268  lgsdinn0  25269  2sqlem9  25351  rpvmasumlem  25375  dchrvmasumiflem1  25389  dchrisum0flblem1  25396  rpvmasum2  25400  pntrsumbnd2  25455  pntleml  25499  tgcgrextend  25579  tgbtwnexch2  25590  tgifscgr  25602  tgcolg  25648  tgidinside  25665  tgbtwnconn1lem2  25667  tgbtwnconn1lem3  25668  lnhl  25709  tglinethru  25730  tglnpt2  25735  tglineneq  25738  coltr  25741  coltr3  25742  colline  25743  mirreu3  25748  miriso  25764  mirln  25770  mirln2  25771  mirconn  25772  mirbtwnhl  25774  colmid  25782  krippenlem  25784  midexlem  25786  ragflat  25798  ragcgr  25801  perprag  25817  perpdragALT  25818  colperpexlem1  25821  colperpexlem3  25823  midex  25828  opphllem1  25838  opphllem2  25839  opphllem5  25842  opphllem6  25843  hlpasch  25847  lmiisolem  25887  hypcgrlem1  25890  hypcgrlem2  25891  cgrg3col4  25933  upgrex  26186  crctcshwlk  26925  crctcsh  26927  1wlkdlem2  27290  eupth2lem3lem3  27382  eupth2lem3lem7  27386  nmcoplbi  29196  nmophmi  29199  nmbdfnlbi  29217  disjdifprg  29695  imadifxp  29721  xlt2addrd  29832  ssnnssfz  29858  psgnfzto1stlem  30159  pmtridf1o  30165  pmtridfv1  30166  pmtridfv2  30167  locfinref  30217  esumpr2  30438  unelldsys  30530  sigapildsyslem  30533  sigapildsys  30534  mbfmcst  30630  carsgsigalem  30686  carsgclctunlem3  30691  pmeasmono  30695  probun  30790  0rrv  30822  sgncl  30909  signsvtn0  30956  signstfvneq0  30958  btwnconn1lem11  32510  finxp00  33550  matunitlindf  33720  poimirlem14  33736  mblfinlem1  33759  mblfinlem2  33760  ismblfin  33763  itg2addnclem  33774  itgaddnclem2  33782  bddiblnc  33793  areacirclem4  33816  areacirc  33818  isbnd3  33896  blbnd  33899  rrnequiv  33947  lsmsat  34798  lkrscss  34888  eqlkr  34889  lkrshpor  34897  atcvrj2b  35221  atltcvr  35224  3dim1  35256  3dim2  35257  3dim3  35258  ps-2  35267  2at0mat0  35314  dalemdnee  35455  dalem63  35524  lnatexN  35568  2llnma3r  35577  pmodlem1  35635  pmapjat1  35642  pclfinclN  35739  osumclN  35756  pexmidALTN  35767  lhpexle2lem  35798  lhpexle3lem  35800  4atexlemex6  35863  4atex  35865  trlnle  35976  trlval3  35977  cdlemc  35987  cdlemd9  35996  cdleme27N  36159  cdleme28c  36162  cdleme32fvaw  36229  cdleme42ke  36275  cdleme42keg  36276  cdleme42mgN  36278  cdleme17d  36288  cdleme48fvg  36290  cdleme50trn123  36344  cdlemb3  36396  cdlemg8  36421  cdlemg15a  36445  cdlemg15  36446  cdlemg16  36447  cdlemg16ALTN  36448  cdlemg16z  36449  cdlemg16zz  36450  cdlemg20  36475  cdlemg22  36477  cdlemg37  36479  cdlemg31d  36490  cdlemg39  36506  cdlemg40  36507  ltrncom  36528  tendotr  36620  cdlemk25-3  36694  cdlemk35s-id  36728  cdlemk39s-id  36730  cdlemk53b  36746  cdlemk53  36747  cdlemk55  36751  cdlemk35u  36754  cdlemk55u  36756  cdlemk39u  36758  cdlemk19u  36760  cdleml5N  36770  dia2dimlem7  36861  dia2dimlem13  36867  dih1dimatlem  37120  dihlsprn  37122  dihjat1lem  37219  dihjat1  37220  dvh2dim  37236  dochexmid  37259  lclkrlem1  37297  lclkrlem2i  37306  lclkrlem2t  37317  lcfrlem34  37367  lcfrlem38  37371  lcfrlem41  37374  mapdindp1  37511  mapdindp2  37512  mapdh6dN  37530  mapdh6jN  37536  mapdh8j  37579  mapdh8  37580  hdmap1l6d  37605  hdmap1l6j  37611  hdmap11lem2  37636  hdmap14lem7  37668  jm2.19  38062  jm2.23  38065  nzss  39018  cnrefiisplem  40558  stoweidlem58  40778  fourierdlem41  40868  fourierdlem48  40874  fouriersw  40951  etransclem24  40978  nnfoctbdjlem  41175  ssnn0ssfz  42637
  Copyright terms: Public domain W3C validator