Theorem pm2.61dane 3046

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

Step	Hyp	Ref	Expression
1		pm2.61dane.1	. . 3 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓)
2	1	ex 418	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
3		pm2.61dane.2	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)
4	3	ex 418	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
5	2, 4	pm2.61dne 3045	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-ne 2960

This theorem is used by:  pm2.61da2ne  3047  pm2.61da3ne  3048  pm2.61iine  3049  disjxiun  5103  onfr  6423  f1oprswap  6896  soex  7960  frxp2  8191  frxp3  8198  riiner  8842  difsnen  9109  mapdom2  9198  nnunifi  9314  fofinf1o  9352  brwdom2  9597  cantnff  9705  cantnfp1  9712  carddomi2  10081  wdomfil  10170  fin1a2lem10  10517  fin1a2lem11  10518  uzsupss  13097  xaddcom  13400  xnegdi  13408  xpncan  13411  xleadd1a  13413  xsubge0  13421  ccat1st1st  14807  swrdccatin1  14905  sgncl  15282  cnpart  15439  fsumcllem  15930  fsumrev2  15980  expcnv  16065  geomulcvg  16077  fprodcllem  16150  fsumdvds  16510  gcd0id  16723  nn0seqcvgd  16777  lcmdvds  16815  mulgcddvds  16862  pcge0  17072  pcneg  17084  pcdvdstr  17086  pcz  17091  pcprmpw2  17092  pcadd  17099  ramcl2  17226  0ramcl  17233  ramub1lem1  17236  ramcl  17239  mrerintcl  17799  mreriincl  17800  mreexexlem4d  17853  mreclatBAD  18769  chnub  18828  psgnunilem1  19740  odmulg  19803  sylow1lem1  19845  pgpfi  19852  odadd1  20095  odadd2  20096  gsumval3  20154  gsumpt  20209  dprdfcntz  20264  dprd2da  20291  ablfac1eulem  20321  pgpfaclem3  20332  ablsimpgfind  20359  abvneg  21116  lssssr  21262  lspsneq  21433  lspdisj2  21438  drngnidl  21564  cnsubrg  21766  matunitlindf  23029  riinopn  23259  riincld  23395  neipeltop  23480  hauscmplem  23757  cmpfi  23759  ptbasfi  23933  xkoccn  23971  txindislem  23985  txtube  23992  hmphindis  24149  fclscmp  24382  utop2nei  24602  nrginvrcn  25044  nmoleub  25083  blcvx  25150  xrsxmet  25162  xrsblre  25164  lebnumlem3  25317  cphsqrtcl2  25540  ovollb2  25843  ioorcl  25931  i1fmulc  26057  itg1mulc  26058  mbfi1fseqlem4  26072  bddiblnc  26195  dvlip  26346  dvne0  26364  ig1pdvds  26531  plyeq0lem  26562  plyeq0  26563  aannenlem2  26689  aalioulem6  26697  abelthlem8  26799  abelth  26801  cxpexp  27029  cxpge0  27044  cxpmul2  27050  abscxp2  27054  abscxpbnd  27114  cxpeq  27118  nnlogbexp  27142  isosctrlem2  27180  atanrecl  27272  wilthlem2  27429  dchrabs2  27622  dchr1re  27623  lgsneg1  27682  lgsdirprm  27691  lgsdir  27692  lgsne0  27695  lgsdirnn0  27704  lgsdinn0  27705  2sqlem9  27787  rpvmasumlem  27847  dchrvmasumiflem1  27861  dchrisum0flblem1  27868  rpvmasum2  27872  pntrsumbnd2  27927  pntleml  27971  tgcgrextend  28980  tgbtwnexch2  28992  tgifscgr  29004  tgcolg  29050  tgidinside  29067  tgbtwnconn1lem2  29069  tgbtwnconn1lem3  29070  lnhl  29114  tglinethru  29137  tglineneq  29146  coltr  29149  coltr3  29150  colline  29151  tglnpt2  29154  tglnpt4  29156  mirreu3  29159  miriso  29175  mirln  29181  mirln2  29182  mirconn  29183  mirbtwnhl  29185  colmid  29193  krippenlem  29195  midexlem  29197  ragflat  29212  ragcgr  29215  perprag  29235  perpdragALT  29236  colperpexlem1  29239  colperpexlem3  29241  midex  29246  opphllem1  29256  opphllem2  29257  opphllem5  29260  opphllem6  29261  hlpasch  29267  lnincplng  29295  lnssplng  29303  mirplncl  29306  lmiisolem  29334  hypcgrlem1  29338  hypcgrlem2  29339  cgrg3col4  29405  prlnghpg  29457  perpprlng  29461  prlngmolem2  29464  prlngpln4  29469  prlngplngtr  29470  prlngmid2  29472  upgrex  29703  crctcshwlk  30444  crctcsh  30446  1wlkdlem2  30762  eupth2lem3lem3  30864  eupth2lem3lem7  30868  nmcoplbi  32663  nmophmi  32666  nmbdfnlbi  32684  cgrgptxfr  33086  tgaas1h  33117  disjdifprg  33244  imadifxp  33270  2ndimaxp  33315  mptiffisupp  33360  xlt2addrd  33424  ssnnssfz  33452  gsumpart  33700  suppgsumssiun  33709  symgcntz  33722  fzo0pmtrlast  33729  pmtridf1o  33731  pmtridfv1  33732  pmtridfv2  33733  psgnfzto1stlem  33737  tocycf  33754  cycpmco2lem5  33767  cycpmco2  33770  fxpgaval  33804  isedom  33934  edomediv  33936  edompid  33941  linds2eq  34020  dvdsruasso  34024  ply1coedeg  34204  ply1degltel  34209  ply1degleel  34210  ig1pmindeg  34217  esplyind  34290  fldext2chn  34443  constraddcl  34477  constrremulcl  34482  constrsqrtcl  34494  cos9thpiminplylem2  34498  locfinref  34556  zarcmplem  34596  esumpr2  34782  unelldsys  34874  sigapildsyslem  34877  sigapildsys  34878  mbfmcst  34974  carsgsigalem  35030  carsgclctunlem3  35035  pmeasmono  35039  probun  35134  0rrv  35166  signsvtn0  35282  signstfvneq0  35284  fineqvac  35897  wevgblacfn  36052  btwnconn1lem11  37053  finxp00  38530  poimirlem14  38757  mblfinlem1  38780  mblfinlem2  38781  ismblfin  38784  itg2addnclem  38794  itgaddnclem2  38802  areacirclem4  38834  areacirc  38836  isbnd3  38921  blbnd  38924  rrnequiv  38972  lsmsat  40268  lkrscss  40358  eqlkr  40359  lkrshpor  40367  atcvrj2b  40692  atltcvr  40695  3dim1  40727  3dim2  40728  3dim3  40729  ps-2  40738  2at0mat0  40785  dalemdnee  40926  dalem63  40995  lnatexN  41039  2llnma3r  41048  pmodlem1  41106  pmapjat1  41113  pclfinclN  41210  osumclN  41227  pexmidALTN  41238  lhpexle2lem  41269  lhpexle3lem  41271  4atexlemex6  41334  4atex  41336  trlnle  41446  trlval3  41447  cdlemc  41457  cdlemd9  41466  cdleme27N  41629  cdleme28c  41632  cdleme32fvaw  41699  cdleme42ke  41745  cdleme42keg  41746  cdleme42mgN  41748  cdleme17d  41758  cdleme48fvg  41760  cdleme50trn123  41814  cdlemb3  41866  cdlemg8  41891  cdlemg15a  41915  cdlemg15  41916  cdlemg16  41917  cdlemg16ALTN  41918  cdlemg16z  41919  cdlemg16zz  41920  cdlemg20  41945  cdlemg22  41947  cdlemg37  41949  cdlemg31d  41960  cdlemg39  41976  cdlemg40  41977  ltrncom  41998  tendotr  42090  cdlemk25-3  42164  cdlemk35s-id  42198  cdlemk39s-id  42200  cdlemk53b  42216  cdlemk53  42217  cdlemk55  42221  cdlemk35u  42224  cdlemk55u  42226  cdlemk39u  42228  cdlemk19u  42230  cdleml5N  42240  dia2dimlem7  42330  dia2dimlem13  42336  dih1dimatlem  42589  dihlsprn  42591  dihjat1lem  42688  dihjat1  42689  dvh2dim  42705  dochexmid  42728  lclkrlem1  42766  lclkrlem2i  42775  lclkrlem2t  42786  lcfrlem34  42836  lcfrlem38  42840  lcfrlem41  42843  mapdindp1  42980  mapdindp2  42981  mapdh6dN  42999  mapdh6jN  43005  mapdh8j  43047  mapdh8  43048  hdmap1l6d  43073  hdmap1l6j  43079  hdmap11lem2  43102  hdmap14lem7  43134  primrootlekpowne0  43358  aks6d1c7lem2  43434  unitscyglem4  43451  jm2.19  44204  jm2.23  44207  nzss  45504  disjxp1  46302  cnrefiisplem  47054  xlimliminflimsup  47087  stoweidlem58  47283  fourierdlem41  47373  fourierdlem48  47379  fouriersw  47456  etransclem24  47483  nnfoctbdjlem  47680  smfpimltxr  47972  smfpimgtxr  48005  chnerlem1  48107  sqrtqaa  48130  ssnn0ssfz  49676  mreclat  50326