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

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ≠ 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 207  df-an 396  df-ne 2933

This theorem is referenced by:  pm2.61da2ne  3020  pm2.61da3ne  3021  pm2.61iine  3022  disjxiun  5116  onfr  6391  f1oprswap  6861  soex  7915  frxp2  8141  frxp3  8148  riiner  8802  difsnen  9065  mapdom2  9160  nnunifi  9297  fofinf1o  9342  brwdom2  9585  cantnff  9686  cantnfp1  9693  carddomi2  9982  wdomfil  10073  fin1a2lem10  10421  fin1a2lem11  10422  uzsupss  12954  xaddcom  13254  xnegdi  13262  xpncan  13265  xleadd1a  13267  xsubge0  13275  ccat1st1st  14644  swrdccatin1  14741  cnpart  15257  fsumcllem  15746  fsumrev2  15796  expcnv  15878  geomulcvg  15890  fprodcllem  15965  fsumdvds  16325  gcd0id  16536  nn0seqcvgd  16587  lcmdvds  16625  mulgcddvds  16672  pcge0  16880  pcneg  16892  pcdvdstr  16894  pcz  16899  pcprmpw2  16900  pcadd  16907  ramcl2  17034  0ramcl  17041  ramub1lem1  17044  ramcl  17047  mrerintcl  17607  mreriincl  17608  mreexexlem4d  17657  mreclatBAD  18571  psgnunilem1  19472  odmulg  19535  sylow1lem1  19577  pgpfi  19584  odadd1  19827  odadd2  19828  gsumval3  19886  gsumpt  19941  dprdfcntz  19996  dprd2da  20023  ablfac1eulem  20053  pgpfaclem3  20064  ablsimpgfind  20091  abvneg  20784  lssssr  20909  lspsneq  21081  lspdisj2  21086  drngnidl  21202  cnsubrg  21393  riinopn  22844  riincld  22980  neipeltop  23065  hauscmplem  23342  cmpfi  23344  ptbasfi  23517  xkoccn  23555  txindislem  23569  txtube  23576  hmphindis  23733  fclscmp  23966  utop2nei  24187  nrginvrcn  24629  nmoleub  24668  blcvx  24735  xrsxmet  24747  xrsblre  24749  lebnumlem3  24911  cphsqrtcl2  25136  ovollb2  25440  ioorcl  25528  i1fmulc  25654  itg1mulc  25655  mbfi1fseqlem4  25669  bddiblnc  25793  dvlip  25948  dvne0  25966  ig1pdvds  26135  plyeq0lem  26165  plyeq0  26166  aannenlem2  26287  aalioulem6  26295  abelthlem8  26399  abelth  26401  cxpexp  26627  cxpge0  26642  cxpmul2  26648  abscxp2  26652  abscxpbnd  26713  cxpeq  26717  nnlogbexp  26741  isosctrlem2  26779  atanrecl  26871  wilthlem2  27029  dchrabs2  27223  dchr1re  27224  lgsneg1  27283  lgsdirprm  27292  lgsdir  27293  lgsne0  27296  lgsdirnn0  27305  lgsdinn0  27306  2sqlem9  27388  rpvmasumlem  27448  dchrvmasumiflem1  27462  dchrisum0flblem1  27469  rpvmasum2  27473  pntrsumbnd2  27528  pntleml  27572  tgcgrextend  28410  tgbtwnexch2  28421  tgifscgr  28433  tgcolg  28479  tgidinside  28496  tgbtwnconn1lem2  28498  tgbtwnconn1lem3  28499  lnhl  28540  tglinethru  28561  tglnpt2  28566  tglineneq  28569  coltr  28572  coltr3  28573  colline  28574  mirreu3  28579  miriso  28595  mirln  28601  mirln2  28602  mirconn  28603  mirbtwnhl  28605  colmid  28613  krippenlem  28615  midexlem  28617  ragflat  28629  ragcgr  28632  perprag  28651  perpdragALT  28652  colperpexlem1  28655  colperpexlem3  28657  midex  28662  opphllem1  28672  opphllem2  28673  opphllem5  28676  opphllem6  28677  hlpasch  28681  lmiisolem  28721  hypcgrlem1  28724  hypcgrlem2  28725  cgrg3col4  28778  upgrex  29017  crctcshwlk  29750  crctcsh  29752  1wlkdlem2  30065  eupth2lem3lem3  30157  eupth2lem3lem7  30161  nmcoplbi  31955  nmophmi  31958  nmbdfnlbi  31976  disjdifprg  32502  imadifxp  32528  2ndimaxp  32570  mptiffisupp  32616  xlt2addrd  32682  ssnnssfz  32710  sgncl  32756  chnub  32938  gsumpart  32997  symgcntz  33042  fzo0pmtrlast  33049  pmtridf1o  33051  pmtridfv1  33052  pmtridfv2  33053  psgnfzto1stlem  33057  tocycf  33074  cycpmco2lem5  33087  cycpmco2  33090  linds2eq  33342  dvdsruasso  33346  ply1degltel  33550  ply1degleel  33551  ig1pmindeg  33557  fldext2chn  33708  constraddcl  33742  constrremulcl  33747  constrsqrtcl  33759  cos9thpiminplylem2  33763  locfinref  33818  zarcmplem  33858  esumpr2  34044  unelldsys  34135  sigapildsyslem  34138  sigapildsys  34139  mbfmcst  34237  carsgsigalem  34293  carsgclctunlem3  34298  pmeasmono  34302  probun  34397  0rrv  34429  signsvtn0  34548  signstfvneq0  34550  fineqvac  35074  wevgblacfn  35077  btwnconn1lem11  36061  finxp00  37366  matunitlindf  37588  poimirlem14  37604  mblfinlem1  37627  mblfinlem2  37628  ismblfin  37631  itg2addnclem  37641  itgaddnclem2  37649  areacirclem4  37681  areacirc  37683  isbnd3  37754  blbnd  37757  rrnequiv  37805  lsmsat  38972  lkrscss  39062  eqlkr  39063  lkrshpor  39071  atcvrj2b  39397  atltcvr  39400  3dim1  39432  3dim2  39433  3dim3  39434  ps-2  39443  2at0mat0  39490  dalemdnee  39631  dalem63  39700  lnatexN  39744  2llnma3r  39753  pmodlem1  39811  pmapjat1  39818  pclfinclN  39915  osumclN  39932  pexmidALTN  39943  lhpexle2lem  39974  lhpexle3lem  39976  4atexlemex6  40039  4atex  40041  trlnle  40151  trlval3  40152  cdlemc  40162  cdlemd9  40171  cdleme27N  40334  cdleme28c  40337  cdleme32fvaw  40404  cdleme42ke  40450  cdleme42keg  40451  cdleme42mgN  40453  cdleme17d  40463  cdleme48fvg  40465  cdleme50trn123  40519  cdlemb3  40571  cdlemg8  40596  cdlemg15a  40620  cdlemg15  40621  cdlemg16  40622  cdlemg16ALTN  40623  cdlemg16z  40624  cdlemg16zz  40625  cdlemg20  40650  cdlemg22  40652  cdlemg37  40654  cdlemg31d  40665  cdlemg39  40681  cdlemg40  40682  ltrncom  40703  tendotr  40795  cdlemk25-3  40869  cdlemk35s-id  40903  cdlemk39s-id  40905  cdlemk53b  40921  cdlemk53  40922  cdlemk55  40926  cdlemk35u  40929  cdlemk55u  40931  cdlemk39u  40933  cdlemk19u  40935  cdleml5N  40945  dia2dimlem7  41035  dia2dimlem13  41041  dih1dimatlem  41294  dihlsprn  41296  dihjat1lem  41393  dihjat1  41394  dvh2dim  41410  dochexmid  41433  lclkrlem1  41471  lclkrlem2i  41480  lclkrlem2t  41491  lcfrlem34  41541  lcfrlem38  41545  lcfrlem41  41548  mapdindp1  41685  mapdindp2  41686  mapdh6dN  41704  mapdh6jN  41710  mapdh8j  41752  mapdh8  41753  hdmap1l6d  41778  hdmap1l6j  41784  hdmap11lem2  41807  hdmap14lem7  41839  primrootlekpowne0  42064  aks6d1c7lem2  42140  unitscyglem4  42157  jm2.19  42964  jm2.23  42967  nzss  44289  disjxp1  45041  cnrefiisplem  45806  xlimliminflimsup  45839  stoweidlem58  46035  fourierdlem41  46125  fourierdlem48  46131  fouriersw  46208  etransclem24  46235  nnfoctbdjlem  46432  smfpimltxr  46724  smfpimgtxr  46757  ssnn0ssfz  48272  mreclat  48919