Theorem pm2.61dane 3020

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  pm2.61da2ne  3021  pm2.61da3ne  3022  pm2.61iine  3023  disjxiun  5083  onfr  6356  f1oprswap  6819  soex  7865  frxp2  8087  frxp3  8094  riiner  8730  difsnen  8990  mapdom2  9079  nnunifi  9194  fofinf1o  9235  brwdom2  9481  cantnff  9586  cantnfp1  9593  carddomi2  9885  wdomfil  9974  fin1a2lem10  10322  fin1a2lem11  10323  uzsupss  12881  xaddcom  13183  xnegdi  13191  xpncan  13194  xleadd1a  13196  xsubge0  13204  ccat1st1st  14582  swrdccatin1  14678  cnpart  15193  fsumcllem  15685  fsumrev2  15735  expcnv  15820  geomulcvg  15832  fprodcllem  15907  fsumdvds  16268  gcd0id  16479  nn0seqcvgd  16530  lcmdvds  16568  mulgcddvds  16615  pcge0  16824  pcneg  16836  pcdvdstr  16838  pcz  16843  pcprmpw2  16844  pcadd  16851  ramcl2  16978  0ramcl  16985  ramub1lem1  16988  ramcl  16991  mrerintcl  17550  mreriincl  17551  mreexexlem4d  17604  mreclatBAD  18520  chnub  18579  psgnunilem1  19459  odmulg  19522  sylow1lem1  19564  pgpfi  19571  odadd1  19814  odadd2  19815  gsumval3  19873  gsumpt  19928  dprdfcntz  19983  dprd2da  20010  ablfac1eulem  20040  pgpfaclem3  20051  ablsimpgfind  20078  abvneg  20794  lssssr  20940  lspsneq  21112  lspdisj2  21117  drngnidl  21233  cnsubrg  21417  riinopn  22883  riincld  23019  neipeltop  23104  hauscmplem  23381  cmpfi  23383  ptbasfi  23556  xkoccn  23594  txindislem  23608  txtube  23615  hmphindis  23772  fclscmp  24005  utop2nei  24225  nrginvrcn  24667  nmoleub  24706  blcvx  24773  xrsxmet  24785  xrsblre  24787  lebnumlem3  24940  cphsqrtcl2  25163  ovollb2  25466  ioorcl  25554  i1fmulc  25680  itg1mulc  25681  mbfi1fseqlem4  25695  bddiblnc  25819  dvlip  25970  dvne0  25988  ig1pdvds  26155  plyeq0lem  26185  plyeq0  26186  aannenlem2  26306  aalioulem6  26314  abelthlem8  26417  abelth  26419  cxpexp  26645  cxpge0  26660  cxpmul2  26666  abscxp2  26670  abscxpbnd  26730  cxpeq  26734  nnlogbexp  26758  isosctrlem2  26796  atanrecl  26888  wilthlem2  27046  dchrabs2  27239  dchr1re  27240  lgsneg1  27299  lgsdirprm  27308  lgsdir  27309  lgsne0  27312  lgsdirnn0  27321  lgsdinn0  27322  2sqlem9  27404  rpvmasumlem  27464  dchrvmasumiflem1  27478  dchrisum0flblem1  27485  rpvmasum2  27489  pntrsumbnd2  27544  pntleml  27588  tgcgrextend  28567  tgbtwnexch2  28578  tgifscgr  28590  tgcolg  28636  tgidinside  28653  tgbtwnconn1lem2  28655  tgbtwnconn1lem3  28656  lnhl  28697  tglinethru  28718  tglnpt2  28723  tglineneq  28726  coltr  28729  coltr3  28730  colline  28731  mirreu3  28736  miriso  28752  mirln  28758  mirln2  28759  mirconn  28760  mirbtwnhl  28762  colmid  28770  krippenlem  28772  midexlem  28774  ragflat  28786  ragcgr  28789  perprag  28808  perpdragALT  28809  colperpexlem1  28812  colperpexlem3  28814  midex  28819  opphllem1  28829  opphllem2  28830  opphllem5  28833  opphllem6  28834  hlpasch  28838  lmiisolem  28878  hypcgrlem1  28881  hypcgrlem2  28882  cgrg3col4  28935  upgrex  29175  crctcshwlk  29905  crctcsh  29907  1wlkdlem2  30223  eupth2lem3lem3  30315  eupth2lem3lem7  30319  nmcoplbi  32114  nmophmi  32117  nmbdfnlbi  32135  disjdifprg  32660  imadifxp  32686  2ndimaxp  32734  mptiffisupp  32781  xlt2addrd  32847  ssnnssfz  32875  sgncl  32919  gsumpart  33139  suppgsumssiun  33148  symgcntz  33161  fzo0pmtrlast  33168  pmtridf1o  33170  pmtridfv1  33171  pmtridfv2  33172  psgnfzto1stlem  33176  tocycf  33193  cycpmco2lem5  33206  cycpmco2  33209  fxpgaval  33243  linds2eq  33456  dvdsruasso  33460  ply1coedeg  33664  ply1degltel  33669  ply1degleel  33670  ig1pmindeg  33677  esplyind  33734  fldext2chn  33888  constraddcl  33922  constrremulcl  33927  constrsqrtcl  33939  cos9thpiminplylem2  33943  locfinref  34001  zarcmplem  34041  esumpr2  34227  unelldsys  34318  sigapildsyslem  34321  sigapildsys  34322  mbfmcst  34419  carsgsigalem  34475  carsgclctunlem3  34480  pmeasmono  34484  probun  34579  0rrv  34611  signsvtn0  34730  signstfvneq0  34732  fineqvac  35276  wevgblacfn  35307  btwnconn1lem11  36295  finxp00  37732  matunitlindf  37953  poimirlem14  37969  mblfinlem1  37992  mblfinlem2  37993  ismblfin  37996  itg2addnclem  38006  itgaddnclem2  38014  areacirclem4  38046  areacirc  38048  isbnd3  38119  blbnd  38122  rrnequiv  38170  lsmsat  39468  lkrscss  39558  eqlkr  39559  lkrshpor  39567  atcvrj2b  39892  atltcvr  39895  3dim1  39927  3dim2  39928  3dim3  39929  ps-2  39938  2at0mat0  39985  dalemdnee  40126  dalem63  40195  lnatexN  40239  2llnma3r  40248  pmodlem1  40306  pmapjat1  40313  pclfinclN  40410  osumclN  40427  pexmidALTN  40438  lhpexle2lem  40469  lhpexle3lem  40471  4atexlemex6  40534  4atex  40536  trlnle  40646  trlval3  40647  cdlemc  40657  cdlemd9  40666  cdleme27N  40829  cdleme28c  40832  cdleme32fvaw  40899  cdleme42ke  40945  cdleme42keg  40946  cdleme42mgN  40948  cdleme17d  40958  cdleme48fvg  40960  cdleme50trn123  41014  cdlemb3  41066  cdlemg8  41091  cdlemg15a  41115  cdlemg15  41116  cdlemg16  41117  cdlemg16ALTN  41118  cdlemg16z  41119  cdlemg16zz  41120  cdlemg20  41145  cdlemg22  41147  cdlemg37  41149  cdlemg31d  41160  cdlemg39  41176  cdlemg40  41177  ltrncom  41198  tendotr  41290  cdlemk25-3  41364  cdlemk35s-id  41398  cdlemk39s-id  41400  cdlemk53b  41416  cdlemk53  41417  cdlemk55  41421  cdlemk35u  41424  cdlemk55u  41426  cdlemk39u  41428  cdlemk19u  41430  cdleml5N  41440  dia2dimlem7  41530  dia2dimlem13  41536  dih1dimatlem  41789  dihlsprn  41791  dihjat1lem  41888  dihjat1  41889  dvh2dim  41905  dochexmid  41928  lclkrlem1  41966  lclkrlem2i  41975  lclkrlem2t  41986  lcfrlem34  42036  lcfrlem38  42040  lcfrlem41  42043  mapdindp1  42180  mapdindp2  42181  mapdh6dN  42199  mapdh6jN  42205  mapdh8j  42247  mapdh8  42248  hdmap1l6d  42273  hdmap1l6j  42279  hdmap11lem2  42302  hdmap14lem7  42334  primrootlekpowne0  42558  aks6d1c7lem2  42634  unitscyglem4  42651  jm2.19  43439  jm2.23  43442  nzss  44762  disjxp1  45518  cnrefiisplem  46275  xlimliminflimsup  46308  stoweidlem58  46504  fourierdlem41  46594  fourierdlem48  46600  fouriersw  46677  etransclem24  46704  nnfoctbdjlem  46901  smfpimltxr  47193  smfpimgtxr  47226  chnerlem1  47328  ssnn0ssfz  48837  mreclat  49484