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 2869
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 2868 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wne 2780
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 196  df-an 385  df-ne 2782
This theorem is referenced by:  pm2.61da2ne  2870  pm2.61da3ne  2871  pm2.61iine  2872  disjxiun  4579  disjxiunOLD  4580  onfr  5680  f1oprswap  6092  soex  7002  riiner  7707  difsnen  7927  mapdom2  8016  nnunifi  8096  fofinf1o  8126  brwdom2  8361  cantnff  8454  cantnfp1  8461  carddomi2  8679  wdomfil  8767  fin1a2lem10  9114  fin1a2lem11  9115  uzsupss  11656  xaddcom  11945  xnegdi  11950  xpncan  11953  xleadd1a  11955  xsubge0  11963  cnpart  13828  fsumcllem  14310  fsumrev2  14356  expcnv  14435  geomulcvg  14446  fprodcllem  14520  fsumdvds  14868  gcd0id  15078  nn0seqcvgd  15121  lcmdvds  15159  mulgcddvds  15207  pcge0  15404  pcneg  15416  pcdvdstr  15418  pcz  15423  pcprmpw2  15424  pcadd  15431  ramcl2  15558  0ramcl  15565  ramub1lem1  15568  ramcl  15571  mrerintcl  16080  mreriincl  16081  mreexexlem4d  16130  mreclatBAD  17010  psgnunilem1  17736  odmulg  17796  sylow1lem1  17836  pgpfi  17843  odadd1  18074  odadd2  18075  gsumval3  18131  gsumpt  18184  dprdfcntz  18237  dprd2da  18264  ablfac1eulem  18294  pgpfaclem3  18305  abvneg  18657  lssssr  18774  lspsneq  18943  lspdisj2  18948  drngnidl  19050  cnsubrg  19625  riinopn  20538  riincld  20658  neipeltop  20743  hauscmplem  21019  cmpfi  21021  ptbasfi  21194  xkoccn  21232  txindislem  21246  txtube  21253  hmphindis  21410  fclscmp  21644  utop2nei  21864  nrginvrcn  22306  nmoleub  22345  blcvx  22409  xrsxmet  22420  xrsblre  22422  lebnumlem3  22570  cphsqrtcl2  22794  ovollb2  23064  ioorcl  23151  i1fmulc  23276  itg1mulc  23277  mbfi1fseqlem4  23291  dvlip  23560  dvne0  23578  ig1pdvds  23740  plyeq0lem  23770  plyeq0  23771  aannenlem2  23888  aalioulem6  23896  abelthlem8  23997  abelth  23999  cxpexp  24214  cxpge0  24229  cxpmul2  24235  abscxp2  24239  abscxpbnd  24294  cxpeq  24298  nnlogbexp  24319  isosctrlem2  24349  atanrecl  24438  wilthlem2  24595  dchrabs2  24787  dchr1re  24788  lgsneg1  24847  lgsdirprm  24856  lgsdir  24857  lgsne0  24860  lgsdirnn0  24869  lgsdinn0  24870  2sqlem9  24952  rpvmasumlem  24976  dchrvmasumiflem1  24990  dchrisum0flblem1  24997  rpvmasum2  25001  pntrsumbnd2  25056  pntleml  25100  tgcgrextend  25180  tgbtwnexch2  25191  tgifscgr  25203  tgcolg  25249  tgidinside  25266  tgbtwnconn1lem2  25268  tgbtwnconn1lem3  25269  lnhl  25310  tglinethru  25331  tglnpt2  25336  tglineneq  25339  coltr  25342  coltr3  25343  colline  25344  mirreu3  25349  miriso  25365  mirln  25371  mirln2  25372  mirconn  25373  mirbtwnhl  25375  colmid  25383  krippenlem  25385  midexlem  25387  ragflat  25399  ragcgr  25402  perprag  25418  perpdragALT  25419  colperpexlem1  25422  colperpexlem3  25424  midex  25429  opphllem1  25439  opphllem2  25440  opphllem5  25443  opphllem6  25444  hlpasch  25448  lmiisolem  25488  hypcgrlem1  25491  hypcgrlem2  25492  cgrg3col4  25534  upgrex  25759  umgraex  25852  eupath2lem3  26506  nmcoplbi  28271  nmophmi  28274  nmbdfnlbi  28292  disjdifprg  28770  imadifxp  28796  xlt2addrd  28913  ssnnssfz  28937  psgnfzto1stlem  29181  locfinref  29236  esumpr2  29456  unelldsys  29548  sigapildsyslem  29551  sigapildsys  29552  mbfmcst  29648  carsgsigalem  29704  carsgclctunlem3  29709  pmeasmono  29713  probun  29808  0rrv  29840  sgncl  29927  signsvtn0  29973  signstfvneq0  29975  btwnconn1lem11  31374  finxp00  32415  matunitlindf  32577  poimirlem14  32593  mblfinlem1  32616  mblfinlem2  32617  ismblfin  32620  itg2addnclem  32631  itgaddnclem2  32639  bddiblnc  32650  areacirclem4  32673  areacirc  32675  isbnd3  32753  blbnd  32756  rrnequiv  32804  lsmsat  33313  lkrscss  33403  eqlkr  33404  lkrshpor  33412  atcvrj2b  33736  atltcvr  33739  3dim1  33771  3dim2  33772  3dim3  33773  ps-2  33782  2at0mat0  33829  dalemdnee  33970  dalem63  34039  lnatexN  34083  2llnma3r  34092  pmodlem1  34150  pmapjat1  34157  pclfinclN  34254  osumclN  34271  pexmidALTN  34282  lhpexle2lem  34313  lhpexle3lem  34315  4atexlemex6  34378  4atex  34380  trlnle  34491  trlval3  34492  cdlemc  34502  cdlemd9  34511  cdleme27N  34675  cdleme28c  34678  cdleme32fvaw  34745  cdleme42ke  34791  cdleme42keg  34792  cdleme42mgN  34794  cdleme17d  34804  cdleme48fvg  34806  cdleme50trn123  34860  cdlemb3  34912  cdlemg8  34937  cdlemg15a  34961  cdlemg15  34962  cdlemg16  34963  cdlemg16ALTN  34964  cdlemg16z  34965  cdlemg16zz  34966  cdlemg20  34991  cdlemg22  34993  cdlemg37  34995  cdlemg31d  35006  cdlemg39  35022  cdlemg40  35023  ltrncom  35044  tendotr  35136  cdlemk25-3  35210  cdlemk35s-id  35244  cdlemk39s-id  35246  cdlemk53b  35262  cdlemk53  35263  cdlemk55  35267  cdlemk35u  35270  cdlemk55u  35272  cdlemk39u  35274  cdlemk19u  35276  cdleml5N  35286  dia2dimlem7  35377  dia2dimlem13  35383  dih1dimatlem  35636  dihlsprn  35638  dihjat1lem  35735  dihjat1  35736  dvh2dim  35752  dochexmid  35775  lclkrlem1  35813  lclkrlem2i  35822  lclkrlem2t  35833  lcfrlem34  35883  lcfrlem38  35887  lcfrlem41  35890  mapdindp1  36027  mapdindp2  36028  mapdh6dN  36046  mapdh6jN  36052  mapdh8j  36095  mapdh8  36096  hdmap1l6d  36121  hdmap1l6j  36127  hdmap11lem2  36152  hdmap14lem7  36184  jm2.19  36578  jm2.23  36581  nzss  37538  stoweidlem58  38951  fourierdlem41  39041  fourierdlem48  39047  fouriersw  39124  etransclem24  39151  nnfoctbdjlem  39348  crctcsh1wlk  41025  crctcsh  41027  11wlkdlem2  41305  eupth2lem3lem3  41398  eupth2lem3lem7  41402  ssnn0ssfz  41920
  Copyright terms: Public domain W3C validator