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 3104
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 413 . 2 (𝜑 → (𝐴 = 𝐵𝜓))
3 pm2.61dane.2 . . 3 ((𝜑𝐴𝐵) → 𝜓)
43ex 413 . 2 (𝜑 → (𝐴𝐵𝜓))
52, 4pm2.61dne 3103 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wne 3016
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 208  df-an 397  df-ne 3017
This theorem is referenced by:  pm2.61da2ne  3105  pm2.61da3ne  3106  pm2.61iine  3107  disjxiun  5055  onfr  6224  f1oprswap  6652  soex  7614  riiner  8360  difsnen  8588  mapdom2  8677  nnunifi  8758  fofinf1o  8788  brwdom2  9026  cantnff  9126  cantnfp1  9133  carddomi2  9388  wdomfil  9476  fin1a2lem10  9820  fin1a2lem11  9821  uzsupss  12329  xaddcom  12623  xnegdi  12631  xpncan  12634  xleadd1a  12636  xsubge0  12644  ccat1st1st  13974  swrdccatin1  14077  cnpart  14589  fsumcllem  15079  fsumrev2  15127  expcnv  15209  geomulcvg  15222  fprodcllem  15295  fsumdvds  15648  gcd0id  15857  nn0seqcvgd  15904  lcmdvds  15942  mulgcddvds  15989  pcge0  16188  pcneg  16200  pcdvdstr  16202  pcz  16207  pcprmpw2  16208  pcadd  16215  ramcl2  16342  0ramcl  16349  ramub1lem1  16352  ramcl  16355  mrerintcl  16858  mreriincl  16859  mreexexlem4d  16908  mreclatBAD  17787  psgnunilem1  18552  odmulg  18614  sylow1lem1  18654  pgpfi  18661  odadd1  18899  odadd2  18900  gsumval3  18958  gsumpt  19013  dprdfcntz  19068  dprd2da  19095  ablfac1eulem  19125  pgpfaclem3  19136  ablsimpgfind  19163  abvneg  19536  lssssr  19656  lspsneq  19825  lspdisj2  19830  drngnidl  19932  cnsubrg  20535  riinopn  21446  riincld  21582  neipeltop  21667  hauscmplem  21944  cmpfi  21946  ptbasfi  22119  xkoccn  22157  txindislem  22171  txtube  22178  hmphindis  22335  fclscmp  22568  utop2nei  22788  nrginvrcn  23230  nmoleub  23269  blcvx  23335  xrsxmet  23346  xrsblre  23348  lebnumlem3  23496  cphsqrtcl2  23719  ovollb2  24019  ioorcl  24107  i1fmulc  24233  itg1mulc  24234  mbfi1fseqlem4  24248  dvlip  24519  dvne0  24537  ig1pdvds  24699  plyeq0lem  24729  plyeq0  24730  aannenlem2  24847  aalioulem6  24855  abelthlem8  24956  abelth  24958  cxpexp  25178  cxpge0  25193  cxpmul2  25199  abscxp2  25203  abscxpbnd  25261  cxpeq  25265  nnlogbexp  25286  isosctrlem2  25324  atanrecl  25416  wilthlem2  25574  dchrabs2  25766  dchr1re  25767  lgsneg1  25826  lgsdirprm  25835  lgsdir  25836  lgsne0  25839  lgsdirnn0  25848  lgsdinn0  25849  2sqlem9  25931  rpvmasumlem  25991  dchrvmasumiflem1  26005  dchrisum0flblem1  26012  rpvmasum2  26016  pntrsumbnd2  26071  pntleml  26115  tgcgrextend  26199  tgbtwnexch2  26210  tgifscgr  26222  tgcolg  26268  tgidinside  26285  tgbtwnconn1lem2  26287  tgbtwnconn1lem3  26288  lnhl  26329  tglinethru  26350  tglnpt2  26355  tglineneq  26358  coltr  26361  coltr3  26362  colline  26363  mirreu3  26368  miriso  26384  mirln  26390  mirln2  26391  mirconn  26392  mirbtwnhl  26394  colmid  26402  krippenlem  26404  midexlem  26406  ragflat  26418  ragcgr  26421  perprag  26440  perpdragALT  26441  colperpexlem1  26444  colperpexlem3  26446  midex  26451  opphllem1  26461  opphllem2  26462  opphllem5  26465  opphllem6  26466  hlpasch  26470  lmiisolem  26510  hypcgrlem1  26513  hypcgrlem2  26514  cgrg3col4  26567  upgrex  26805  crctcshwlk  27528  crctcsh  27530  1wlkdlem2  27845  eupth2lem3lem3  27937  eupth2lem3lem7  27941  nmcoplbi  29733  nmophmi  29736  nmbdfnlbi  29754  disjdifprg  30254  imadifxp  30280  xlt2addrd  30409  ssnnssfz  30437  symgcntz  30657  pmtridf1o  30664  pmtridfv1  30665  pmtridfv2  30666  psgnfzto1stlem  30670  tocycf  30687  cycpmco2lem5  30700  cycpmco2  30703  linds2eq  30869  locfinref  31005  esumpr2  31226  unelldsys  31317  sigapildsyslem  31320  sigapildsys  31321  mbfmcst  31417  carsgsigalem  31473  carsgclctunlem3  31478  pmeasmono  31482  probun  31577  0rrv  31609  sgncl  31696  signsvtn0  31740  signstfvneq0  31742  btwnconn1lem11  33456  finxp00  34566  matunitlindf  34772  poimirlem14  34788  mblfinlem1  34811  mblfinlem2  34812  ismblfin  34815  itg2addnclem  34825  itgaddnclem2  34833  bddiblnc  34844  areacirclem4  34867  areacirc  34869  isbnd3  34945  blbnd  34948  rrnequiv  34996  lsmsat  36026  lkrscss  36116  eqlkr  36117  lkrshpor  36125  atcvrj2b  36450  atltcvr  36453  3dim1  36485  3dim2  36486  3dim3  36487  ps-2  36496  2at0mat0  36543  dalemdnee  36684  dalem63  36753  lnatexN  36797  2llnma3r  36806  pmodlem1  36864  pmapjat1  36871  pclfinclN  36968  osumclN  36985  pexmidALTN  36996  lhpexle2lem  37027  lhpexle3lem  37029  4atexlemex6  37092  4atex  37094  trlnle  37204  trlval3  37205  cdlemc  37215  cdlemd9  37224  cdleme27N  37387  cdleme28c  37390  cdleme32fvaw  37457  cdleme42ke  37503  cdleme42keg  37504  cdleme42mgN  37506  cdleme17d  37516  cdleme48fvg  37518  cdleme50trn123  37572  cdlemb3  37624  cdlemg8  37649  cdlemg15a  37673  cdlemg15  37674  cdlemg16  37675  cdlemg16ALTN  37676  cdlemg16z  37677  cdlemg16zz  37678  cdlemg20  37703  cdlemg22  37705  cdlemg37  37707  cdlemg31d  37718  cdlemg39  37734  cdlemg40  37735  ltrncom  37756  tendotr  37848  cdlemk25-3  37922  cdlemk35s-id  37956  cdlemk39s-id  37958  cdlemk53b  37974  cdlemk53  37975  cdlemk55  37979  cdlemk35u  37982  cdlemk55u  37984  cdlemk39u  37986  cdlemk19u  37988  cdleml5N  37998  dia2dimlem7  38088  dia2dimlem13  38094  dih1dimatlem  38347  dihlsprn  38349  dihjat1lem  38446  dihjat1  38447  dvh2dim  38463  dochexmid  38486  lclkrlem1  38524  lclkrlem2i  38533  lclkrlem2t  38544  lcfrlem34  38594  lcfrlem38  38598  lcfrlem41  38601  mapdindp1  38738  mapdindp2  38739  mapdh6dN  38757  mapdh6jN  38763  mapdh8j  38805  mapdh8  38806  hdmap1l6d  38831  hdmap1l6j  38837  hdmap11lem2  38860  hdmap14lem7  38892  jm2.19  39470  jm2.23  39473  nzss  40529  disjxp1  41211  cnrefiisplem  41990  xlimliminflimsup  42023  stoweidlem58  42224  fourierdlem41  42314  fourierdlem48  42320  fouriersw  42397  etransclem24  42424  nnfoctbdjlem  42618  ssnn0ssfz  44295
  Copyright terms: Public domain W3C validator