Theorem pm2.61dane 3015

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ≠ wne 2928

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 2929

This theorem is referenced by:  pm2.61da2ne  3016  pm2.61da3ne  3017  pm2.61iine  3018  disjxiun  5088  onfr  6345  f1oprswap  6807  soex  7851  frxp2  8074  frxp3  8081  riiner  8714  difsnen  8972  mapdom2  9061  nnunifi  9175  fofinf1o  9216  brwdom2  9459  cantnff  9564  cantnfp1  9571  carddomi2  9860  wdomfil  9949  fin1a2lem10  10297  fin1a2lem11  10298  uzsupss  12835  xaddcom  13136  xnegdi  13144  xpncan  13147  xleadd1a  13149  xsubge0  13157  ccat1st1st  14533  swrdccatin1  14629  cnpart  15144  fsumcllem  15636  fsumrev2  15686  expcnv  15768  geomulcvg  15780  fprodcllem  15855  fsumdvds  16216  gcd0id  16427  nn0seqcvgd  16478  lcmdvds  16516  mulgcddvds  16563  pcge0  16771  pcneg  16783  pcdvdstr  16785  pcz  16790  pcprmpw2  16791  pcadd  16798  ramcl2  16925  0ramcl  16932  ramub1lem1  16935  ramcl  16938  mrerintcl  17496  mreriincl  17497  mreexexlem4d  17550  mreclatBAD  18466  chnub  18525  psgnunilem1  19403  odmulg  19466  sylow1lem1  19508  pgpfi  19515  odadd1  19758  odadd2  19759  gsumval3  19817  gsumpt  19872  dprdfcntz  19927  dprd2da  19954  ablfac1eulem  19984  pgpfaclem3  19995  ablsimpgfind  20022  abvneg  20739  lssssr  20885  lspsneq  21057  lspdisj2  21062  drngnidl  21178  cnsubrg  21362  riinopn  22821  riincld  22957  neipeltop  23042  hauscmplem  23319  cmpfi  23321  ptbasfi  23494  xkoccn  23532  txindislem  23546  txtube  23553  hmphindis  23710  fclscmp  23943  utop2nei  24163  nrginvrcn  24605  nmoleub  24644  blcvx  24711  xrsxmet  24723  xrsblre  24725  lebnumlem3  24887  cphsqrtcl2  25111  ovollb2  25415  ioorcl  25503  i1fmulc  25629  itg1mulc  25630  mbfi1fseqlem4  25644  bddiblnc  25768  dvlip  25923  dvne0  25941  ig1pdvds  26110  plyeq0lem  26140  plyeq0  26141  aannenlem2  26262  aalioulem6  26270  abelthlem8  26374  abelth  26376  cxpexp  26602  cxpge0  26617  cxpmul2  26623  abscxp2  26627  abscxpbnd  26688  cxpeq  26692  nnlogbexp  26716  isosctrlem2  26754  atanrecl  26846  wilthlem2  27004  dchrabs2  27198  dchr1re  27199  lgsneg1  27258  lgsdirprm  27267  lgsdir  27268  lgsne0  27271  lgsdirnn0  27280  lgsdinn0  27281  2sqlem9  27363  rpvmasumlem  27423  dchrvmasumiflem1  27437  dchrisum0flblem1  27444  rpvmasum2  27448  pntrsumbnd2  27503  pntleml  27547  tgcgrextend  28461  tgbtwnexch2  28472  tgifscgr  28484  tgcolg  28530  tgidinside  28547  tgbtwnconn1lem2  28549  tgbtwnconn1lem3  28550  lnhl  28591  tglinethru  28612  tglnpt2  28617  tglineneq  28620  coltr  28623  coltr3  28624  colline  28625  mirreu3  28630  miriso  28646  mirln  28652  mirln2  28653  mirconn  28654  mirbtwnhl  28656  colmid  28664  krippenlem  28666  midexlem  28668  ragflat  28680  ragcgr  28683  perprag  28702  perpdragALT  28703  colperpexlem1  28706  colperpexlem3  28708  midex  28713  opphllem1  28723  opphllem2  28724  opphllem5  28727  opphllem6  28728  hlpasch  28732  lmiisolem  28772  hypcgrlem1  28775  hypcgrlem2  28776  cgrg3col4  28829  upgrex  29068  crctcshwlk  29798  crctcsh  29800  1wlkdlem2  30113  eupth2lem3lem3  30205  eupth2lem3lem7  30209  nmcoplbi  32003  nmophmi  32006  nmbdfnlbi  32024  disjdifprg  32550  imadifxp  32576  2ndimaxp  32623  mptiffisupp  32669  xlt2addrd  32737  ssnnssfz  32765  sgncl  32809  gsumpart  33032  symgcntz  33049  fzo0pmtrlast  33056  pmtridf1o  33058  pmtridfv1  33059  pmtridfv2  33060  psgnfzto1stlem  33064  tocycf  33081  cycpmco2lem5  33094  cycpmco2  33097  fxpgaval  33131  linds2eq  33341  dvdsruasso  33345  ply1degltel  33550  ply1degleel  33551  ig1pmindeg  33557  fldext2chn  33736  constraddcl  33770  constrremulcl  33775  constrsqrtcl  33787  cos9thpiminplylem2  33791  locfinref  33849  zarcmplem  33889  esumpr2  34075  unelldsys  34166  sigapildsyslem  34169  sigapildsys  34170  mbfmcst  34267  carsgsigalem  34323  carsgclctunlem3  34328  pmeasmono  34332  probun  34427  0rrv  34459  signsvtn0  34578  signstfvneq0  34580  fineqvac  35127  wevgblacfn  35141  btwnconn1lem11  36130  finxp00  37435  matunitlindf  37657  poimirlem14  37673  mblfinlem1  37696  mblfinlem2  37697  ismblfin  37700  itg2addnclem  37710  itgaddnclem2  37718  areacirclem4  37750  areacirc  37752  isbnd3  37823  blbnd  37826  rrnequiv  37874  lsmsat  39046  lkrscss  39136  eqlkr  39137  lkrshpor  39145  atcvrj2b  39470  atltcvr  39473  3dim1  39505  3dim2  39506  3dim3  39507  ps-2  39516  2at0mat0  39563  dalemdnee  39704  dalem63  39773  lnatexN  39817  2llnma3r  39826  pmodlem1  39884  pmapjat1  39891  pclfinclN  39988  osumclN  40005  pexmidALTN  40016  lhpexle2lem  40047  lhpexle3lem  40049  4atexlemex6  40112  4atex  40114  trlnle  40224  trlval3  40225  cdlemc  40235  cdlemd9  40244  cdleme27N  40407  cdleme28c  40410  cdleme32fvaw  40477  cdleme42ke  40523  cdleme42keg  40524  cdleme42mgN  40526  cdleme17d  40536  cdleme48fvg  40538  cdleme50trn123  40592  cdlemb3  40644  cdlemg8  40669  cdlemg15a  40693  cdlemg15  40694  cdlemg16  40695  cdlemg16ALTN  40696  cdlemg16z  40697  cdlemg16zz  40698  cdlemg20  40723  cdlemg22  40725  cdlemg37  40727  cdlemg31d  40738  cdlemg39  40754  cdlemg40  40755  ltrncom  40776  tendotr  40868  cdlemk25-3  40942  cdlemk35s-id  40976  cdlemk39s-id  40978  cdlemk53b  40994  cdlemk53  40995  cdlemk55  40999  cdlemk35u  41002  cdlemk55u  41004  cdlemk39u  41006  cdlemk19u  41008  cdleml5N  41018  dia2dimlem7  41108  dia2dimlem13  41114  dih1dimatlem  41367  dihlsprn  41369  dihjat1lem  41466  dihjat1  41467  dvh2dim  41483  dochexmid  41506  lclkrlem1  41544  lclkrlem2i  41553  lclkrlem2t  41564  lcfrlem34  41614  lcfrlem38  41618  lcfrlem41  41621  mapdindp1  41758  mapdindp2  41759  mapdh6dN  41777  mapdh6jN  41783  mapdh8j  41825  mapdh8  41826  hdmap1l6d  41851  hdmap1l6j  41857  hdmap11lem2  41880  hdmap14lem7  41912  primrootlekpowne0  42137  aks6d1c7lem2  42213  unitscyglem4  42230  jm2.19  43025  jm2.23  43028  nzss  44349  disjxp1  45105  cnrefiisplem  45866  xlimliminflimsup  45899  stoweidlem58  46095  fourierdlem41  46185  fourierdlem48  46191  fouriersw  46268  etransclem24  46295  nnfoctbdjlem  46492  smfpimltxr  46784  smfpimgtxr  46817  ssnn0ssfz  48379  mreclat  49027