Theorem pm2.61dane 3043

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 3042	1 ⊢ (𝜑 → 𝜓)

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

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 2957

This theorem is used by:  pm2.61da2ne  3044  pm2.61da3ne  3045  pm2.61iine  3046  disjxiun  5100  onfr  6395  f1oprswap  6862  soex  7922  frxp2  8145  frxp3  8152  riiner  8795  difsnen  9062  mapdom2  9151  nnunifi  9267  fofinf1o  9305  brwdom2  9551  cantnff  9659  cantnfp1  9666  carddomi2  10032  wdomfil  10121  fin1a2lem10  10468  fin1a2lem11  10469  uzsupss  13048  xaddcom  13351  xnegdi  13359  xpncan  13362  xleadd1a  13364  xsubge0  13372  ccat1st1st  14756  swrdccatin1  14854  sgncl  15230  cnpart  15387  fsumcllem  15878  fsumrev2  15928  expcnv  16013  geomulcvg  16025  fprodcllem  16098  fsumdvds  16458  gcd0id  16671  nn0seqcvgd  16725  lcmdvds  16763  mulgcddvds  16810  pcge0  17020  pcneg  17032  pcdvdstr  17034  pcz  17039  pcprmpw2  17040  pcadd  17047  ramcl2  17174  0ramcl  17181  ramub1lem1  17184  ramcl  17187  mrerintcl  17747  mreriincl  17748  mreexexlem4d  17801  mreclatBAD  18717  chnub  18776  psgnunilem1  19687  odmulg  19750  sylow1lem1  19792  pgpfi  19799  odadd1  20042  odadd2  20043  gsumval3  20101  gsumpt  20156  dprdfcntz  20211  dprd2da  20238  ablfac1eulem  20268  pgpfaclem3  20279  ablsimpgfind  20306  abvneg  21063  lssssr  21209  lspsneq  21380  lspdisj2  21385  drngnidl  21511  cnsubrg  21713  matunitlindf  22976  riinopn  23206  riincld  23342  neipeltop  23427  hauscmplem  23704  cmpfi  23706  ptbasfi  23880  xkoccn  23918  txindislem  23932  txtube  23939  hmphindis  24096  fclscmp  24329  utop2nei  24549  nrginvrcn  24991  nmoleub  25030  blcvx  25097  xrsxmet  25109  xrsblre  25111  lebnumlem3  25264  cphsqrtcl2  25487  ovollb2  25790  ioorcl  25878  i1fmulc  26004  itg1mulc  26005  mbfi1fseqlem4  26019  bddiblnc  26142  dvlip  26293  dvne0  26311  ig1pdvds  26478  plyeq0lem  26509  plyeq0  26510  aannenlem2  26638  aalioulem6  26646  abelthlem8  26748  abelth  26750  cxpexp  26978  cxpge0  26993  cxpmul2  26999  abscxp2  27003  abscxpbnd  27063  cxpeq  27067  nnlogbexp  27091  isosctrlem2  27129  atanrecl  27221  wilthlem2  27378  dchrabs2  27571  dchr1re  27572  lgsneg1  27631  lgsdirprm  27640  lgsdir  27641  lgsne0  27644  lgsdirnn0  27653  lgsdinn0  27654  2sqlem9  27736  rpvmasumlem  27796  dchrvmasumiflem1  27810  dchrisum0flblem1  27817  rpvmasum2  27821  pntrsumbnd2  27876  pntleml  27920  tgcgrextend  28929  tgbtwnexch2  28941  tgifscgr  28953  tgcolg  28999  tgidinside  29016  tgbtwnconn1lem2  29018  tgbtwnconn1lem3  29019  lnhl  29063  tglinethru  29086  tglineneq  29095  coltr  29098  coltr3  29099  colline  29100  tglnpt2  29103  tglnpt4  29105  mirreu3  29108  miriso  29124  mirln  29130  mirln2  29131  mirconn  29132  mirbtwnhl  29134  colmid  29142  krippenlem  29144  midexlem  29146  ragflat  29161  ragcgr  29164  perprag  29184  perpdragALT  29185  colperpexlem1  29188  colperpexlem3  29190  midex  29195  opphllem1  29205  opphllem2  29206  opphllem5  29209  opphllem6  29210  hlpasch  29216  lnincplng  29244  lnssplng  29252  mirplncl  29255  lmiisolem  29283  hypcgrlem1  29287  hypcgrlem2  29288  cgrg3col4  29354  prlnghpg  29406  perpprlng  29410  prlngmolem2  29413  prlngpln4  29418  prlngplngtr  29419  prlngmid2  29421  upgrex  29652  crctcshwlk  30393  crctcsh  30395  1wlkdlem2  30711  eupth2lem3lem3  30813  eupth2lem3lem7  30817  nmcoplbi  32612  nmophmi  32615  nmbdfnlbi  32633  disjdifprg  33151  imadifxp  33177  2ndimaxp  33222  mptiffisupp  33268  xlt2addrd  33333  ssnnssfz  33361  gsumpart  33606  suppgsumssiun  33615  symgcntz  33628  fzo0pmtrlast  33635  pmtridf1o  33637  pmtridfv1  33638  pmtridfv2  33639  psgnfzto1stlem  33643  tocycf  33660  cycpmco2lem5  33673  cycpmco2  33676  fxpgaval  33710  linds2eq  33918  dvdsruasso  33922  ply1coedeg  34103  ply1degltel  34108  ply1degleel  34109  ig1pmindeg  34116  esplyind  34189  fldext2chn  34342  constraddcl  34376  constrremulcl  34381  constrsqrtcl  34393  cos9thpiminplylem2  34397  locfinref  34455  zarcmplem  34495  esumpr2  34681  unelldsys  34773  sigapildsyslem  34776  sigapildsys  34777  mbfmcst  34874  carsgsigalem  34930  carsgclctunlem3  34935  pmeasmono  34939  probun  35034  0rrv  35066  signsvtn0  35182  signstfvneq0  35184  fineqvac  35757  wevgblacfn  35863  btwnconn1lem11  36832  finxp00  38293  poimirlem14  38520  mblfinlem1  38543  mblfinlem2  38544  ismblfin  38547  itg2addnclem  38557  itgaddnclem2  38565  areacirclem4  38597  areacirc  38599  isbnd3  38686  blbnd  38689  rrnequiv  38737  lsmsat  40033  lkrscss  40123  eqlkr  40124  lkrshpor  40132  atcvrj2b  40457  atltcvr  40460  3dim1  40492  3dim2  40493  3dim3  40494  ps-2  40503  2at0mat0  40550  dalemdnee  40691  dalem63  40760  lnatexN  40804  2llnma3r  40813  pmodlem1  40871  pmapjat1  40878  pclfinclN  40975  osumclN  40992  pexmidALTN  41003  lhpexle2lem  41034  lhpexle3lem  41036  4atexlemex6  41099  4atex  41101  trlnle  41211  trlval3  41212  cdlemc  41222  cdlemd9  41231  cdleme27N  41394  cdleme28c  41397  cdleme32fvaw  41464  cdleme42ke  41510  cdleme42keg  41511  cdleme42mgN  41513  cdleme17d  41523  cdleme48fvg  41525  cdleme50trn123  41579  cdlemb3  41631  cdlemg8  41656  cdlemg15a  41680  cdlemg15  41681  cdlemg16  41682  cdlemg16ALTN  41683  cdlemg16z  41684  cdlemg16zz  41685  cdlemg20  41710  cdlemg22  41712  cdlemg37  41714  cdlemg31d  41725  cdlemg39  41741  cdlemg40  41742  ltrncom  41763  tendotr  41855  cdlemk25-3  41929  cdlemk35s-id  41963  cdlemk39s-id  41965  cdlemk53b  41981  cdlemk53  41982  cdlemk55  41986  cdlemk35u  41989  cdlemk55u  41991  cdlemk39u  41993  cdlemk19u  41995  cdleml5N  42005  dia2dimlem7  42095  dia2dimlem13  42101  dih1dimatlem  42354  dihlsprn  42356  dihjat1lem  42453  dihjat1  42454  dvh2dim  42470  dochexmid  42493  lclkrlem1  42531  lclkrlem2i  42540  lclkrlem2t  42551  lcfrlem34  42601  lcfrlem38  42605  lcfrlem41  42608  mapdindp1  42745  mapdindp2  42746  mapdh6dN  42764  mapdh6jN  42770  mapdh8j  42812  mapdh8  42813  hdmap1l6d  42838  hdmap1l6j  42844  hdmap11lem2  42867  hdmap14lem7  42899  primrootlekpowne0  43123  aks6d1c7lem2  43199  unitscyglem4  43216  jm2.19  43953  jm2.23  43956  nzss  45260  disjxp1  46029  cnrefiisplem  46783  xlimliminflimsup  46816  stoweidlem58  47012  fourierdlem41  47102  fourierdlem48  47108  fouriersw  47185  etransclem24  47212  nnfoctbdjlem  47409  smfpimltxr  47701  smfpimgtxr  47734  chnerlem1  47836  sqrtqaa  47859  ssnn0ssfz  49405  mreclat  50049