Theorem pm2.61dane 3018

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 411	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
3		pm2.61dane.2	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)
4	3	ex 411	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
5	2, 4	pm2.61dne 3017	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ≠ wne 2929

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 206  df-an 395  df-ne 2930

This theorem is referenced by:  pm2.61da2ne  3019  pm2.61da3ne  3020  pm2.61iine  3021  disjxiun  5149  onfr  6414  f1oprswap  6886  soex  7933  frxp2  8157  frxp3  8164  riiner  8818  difsnen  9090  mapdom2  9185  nnunifi  9331  fofinf1o  9367  brwdom2  9612  cantnff  9713  cantnfp1  9720  carddomi2  10009  wdomfil  10100  fin1a2lem10  10448  fin1a2lem11  10449  uzsupss  12971  xaddcom  13268  xnegdi  13276  xpncan  13279  xleadd1a  13281  xsubge0  13289  ccat1st1st  14631  swrdccatin1  14728  cnpart  15240  fsumcllem  15731  fsumrev2  15781  expcnv  15863  geomulcvg  15875  fprodcllem  15948  fsumdvds  16305  gcd0id  16514  nn0seqcvgd  16566  lcmdvds  16604  mulgcddvds  16651  pcge0  16859  pcneg  16871  pcdvdstr  16873  pcz  16878  pcprmpw2  16879  pcadd  16886  ramcl2  17013  0ramcl  17020  ramub1lem1  17023  ramcl  17026  mrerintcl  17605  mreriincl  17606  mreexexlem4d  17655  mreclatBAD  18583  psgnunilem1  19486  odmulg  19549  sylow1lem1  19591  pgpfi  19598  odadd1  19841  odadd2  19842  gsumval3  19900  gsumpt  19955  dprdfcntz  20010  dprd2da  20037  ablfac1eulem  20067  pgpfaclem3  20078  ablsimpgfind  20105  abvneg  20754  lssssr  20878  lspsneq  21050  lspdisj2  21055  drngnidl  21179  cnsubrg  21416  riinopn  22893  riincld  23031  neipeltop  23116  hauscmplem  23393  cmpfi  23395  ptbasfi  23568  xkoccn  23606  txindislem  23620  txtube  23627  hmphindis  23784  fclscmp  24017  utop2nei  24238  nrginvrcn  24692  nmoleub  24731  blcvx  24797  xrsxmet  24808  xrsblre  24810  lebnumlem3  24972  cphsqrtcl2  25197  ovollb2  25501  ioorcl  25589  i1fmulc  25716  itg1mulc  25717  mbfi1fseqlem4  25731  bddiblnc  25854  dvlip  26009  dvne0  26027  ig1pdvds  26199  plyeq0lem  26229  plyeq0  26230  aannenlem2  26349  aalioulem6  26357  abelthlem8  26461  abelth  26463  cxpexp  26687  cxpge0  26702  cxpmul2  26708  abscxp2  26712  abscxpbnd  26773  cxpeq  26777  nnlogbexp  26801  isosctrlem2  26839  atanrecl  26931  wilthlem2  27089  dchrabs2  27283  dchr1re  27284  lgsneg1  27343  lgsdirprm  27352  lgsdir  27353  lgsne0  27356  lgsdirnn0  27365  lgsdinn0  27366  2sqlem9  27448  rpvmasumlem  27508  dchrvmasumiflem1  27522  dchrisum0flblem1  27529  rpvmasum2  27533  pntrsumbnd2  27588  pntleml  27632  tgcgrextend  28404  tgbtwnexch2  28415  tgifscgr  28427  tgcolg  28473  tgidinside  28490  tgbtwnconn1lem2  28492  tgbtwnconn1lem3  28493  lnhl  28534  tglinethru  28555  tglnpt2  28560  tglineneq  28563  coltr  28566  coltr3  28567  colline  28568  mirreu3  28573  miriso  28589  mirln  28595  mirln2  28596  mirconn  28597  mirbtwnhl  28599  colmid  28607  krippenlem  28609  midexlem  28611  ragflat  28623  ragcgr  28626  perprag  28645  perpdragALT  28646  colperpexlem1  28649  colperpexlem3  28651  midex  28656  opphllem1  28666  opphllem2  28667  opphllem5  28670  opphllem6  28671  hlpasch  28675  lmiisolem  28715  hypcgrlem1  28718  hypcgrlem2  28719  cgrg3col4  28772  upgrex  29020  crctcshwlk  29748  crctcsh  29750  1wlkdlem2  30063  eupth2lem3lem3  30155  eupth2lem3lem7  30159  nmcoplbi  31953  nmophmi  31956  nmbdfnlbi  31974  disjdifprg  32486  imadifxp  32512  2ndimaxp  32555  mptiffisupp  32596  xlt2addrd  32651  ssnnssfz  32678  chnub  32870  gsumpart  32912  symgcntz  32951  fzo0pmtrlast  32958  pmtridf1o  32960  pmtridfv1  32961  pmtridfv2  32962  psgnfzto1stlem  32966  tocycf  32983  cycpmco2lem5  32996  cycpmco2  32999  linds2eq  33244  dvdsruasso  33248  ply1degltel  33445  ply1degleel  33446  ig1pmindeg  33452  fldext2chn  33574  locfinref  33624  zarcmplem  33664  esumpr2  33868  unelldsys  33959  sigapildsyslem  33962  sigapildsys  33963  mbfmcst  34061  carsgsigalem  34117  carsgclctunlem3  34122  pmeasmono  34126  probun  34221  0rrv  34253  sgncl  34340  signsvtn0  34384  signstfvneq0  34386  fineqvac  34899  btwnconn1lem11  35881  finxp00  37069  matunitlindf  37279  poimirlem14  37295  mblfinlem1  37318  mblfinlem2  37319  ismblfin  37322  itg2addnclem  37332  itgaddnclem2  37340  areacirclem4  37372  areacirc  37374  isbnd3  37445  blbnd  37448  rrnequiv  37496  lsmsat  38666  lkrscss  38756  eqlkr  38757  lkrshpor  38765  atcvrj2b  39091  atltcvr  39094  3dim1  39126  3dim2  39127  3dim3  39128  ps-2  39137  2at0mat0  39184  dalemdnee  39325  dalem63  39394  lnatexN  39438  2llnma3r  39447  pmodlem1  39505  pmapjat1  39512  pclfinclN  39609  osumclN  39626  pexmidALTN  39637  lhpexle2lem  39668  lhpexle3lem  39670  4atexlemex6  39733  4atex  39735  trlnle  39845  trlval3  39846  cdlemc  39856  cdlemd9  39865  cdleme27N  40028  cdleme28c  40031  cdleme32fvaw  40098  cdleme42ke  40144  cdleme42keg  40145  cdleme42mgN  40147  cdleme17d  40157  cdleme48fvg  40159  cdleme50trn123  40213  cdlemb3  40265  cdlemg8  40290  cdlemg15a  40314  cdlemg15  40315  cdlemg16  40316  cdlemg16ALTN  40317  cdlemg16z  40318  cdlemg16zz  40319  cdlemg20  40344  cdlemg22  40346  cdlemg37  40348  cdlemg31d  40359  cdlemg39  40375  cdlemg40  40376  ltrncom  40397  tendotr  40489  cdlemk25-3  40563  cdlemk35s-id  40597  cdlemk39s-id  40599  cdlemk53b  40615  cdlemk53  40616  cdlemk55  40620  cdlemk35u  40623  cdlemk55u  40625  cdlemk39u  40627  cdlemk19u  40629  cdleml5N  40639  dia2dimlem7  40729  dia2dimlem13  40735  dih1dimatlem  40988  dihlsprn  40990  dihjat1lem  41087  dihjat1  41088  dvh2dim  41104  dochexmid  41127  lclkrlem1  41165  lclkrlem2i  41174  lclkrlem2t  41185  lcfrlem34  41235  lcfrlem38  41239  lcfrlem41  41242  mapdindp1  41379  mapdindp2  41380  mapdh6dN  41398  mapdh6jN  41404  mapdh8j  41446  mapdh8  41447  hdmap1l6d  41472  hdmap1l6j  41478  hdmap11lem2  41501  hdmap14lem7  41533  primrootlekpowne0  41763  aks6d1c7lem2  41839  jm2.19  42600  jm2.23  42603  nzss  43940  disjxp1  44619  cnrefiisplem  45399  xlimliminflimsup  45432  stoweidlem58  45628  fourierdlem41  45718  fourierdlem48  45724  fouriersw  45801  etransclem24  45828  nnfoctbdjlem  46025  smfpimltxr  46317  smfpimgtxr  46350  ssnn0ssfz  47677  mreclat  48272