Theorem pm2.61dane 3032

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ≠ wne 2943

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 397  df-ne 2944

This theorem is referenced by:  pm2.61da2ne  3033  pm2.61da3ne  3034  pm2.61iine  3035  disjxiun  5071  onfr  6299  f1oprswap  6753  soex  7759  riiner  8567  difsnen  8828  mapdom2  8923  nnunifi  9053  fofinf1o  9082  brwdom2  9320  cantnff  9420  cantnfp1  9427  carddomi2  9716  wdomfil  9805  fin1a2lem10  10153  fin1a2lem11  10154  uzsupss  12668  xaddcom  12962  xnegdi  12970  xpncan  12973  xleadd1a  12975  xsubge0  12983  ccat1st1st  14323  swrdccatin1  14426  cnpart  14939  fsumcllem  15432  fsumrev2  15482  expcnv  15564  geomulcvg  15576  fprodcllem  15649  fsumdvds  16005  gcd0id  16214  nn0seqcvgd  16263  lcmdvds  16301  mulgcddvds  16348  pcge0  16551  pcneg  16563  pcdvdstr  16565  pcz  16570  pcprmpw2  16571  pcadd  16578  ramcl2  16705  0ramcl  16712  ramub1lem1  16715  ramcl  16718  mrerintcl  17294  mreriincl  17295  mreexexlem4d  17344  mreclatBAD  18269  psgnunilem1  19089  odmulg  19151  sylow1lem1  19191  pgpfi  19198  odadd1  19437  odadd2  19438  gsumval3  19496  gsumpt  19551  dprdfcntz  19606  dprd2da  19633  ablfac1eulem  19663  pgpfaclem3  19674  ablsimpgfind  19701  abvneg  20082  lssssr  20203  lspsneq  20372  lspdisj2  20377  drngnidl  20488  cnsubrg  20646  riinopn  22045  riincld  22183  neipeltop  22268  hauscmplem  22545  cmpfi  22547  ptbasfi  22720  xkoccn  22758  txindislem  22772  txtube  22779  hmphindis  22936  fclscmp  23169  utop2nei  23390  nrginvrcn  23844  nmoleub  23883  blcvx  23949  xrsxmet  23960  xrsblre  23962  lebnumlem3  24114  cphsqrtcl2  24338  ovollb2  24641  ioorcl  24729  i1fmulc  24856  itg1mulc  24857  mbfi1fseqlem4  24871  bddiblnc  24994  dvlip  25145  dvne0  25163  ig1pdvds  25329  plyeq0lem  25359  plyeq0  25360  aannenlem2  25477  aalioulem6  25485  abelthlem8  25586  abelth  25588  cxpexp  25811  cxpge0  25826  cxpmul2  25832  abscxp2  25836  abscxpbnd  25894  cxpeq  25898  nnlogbexp  25919  isosctrlem2  25957  atanrecl  26049  wilthlem2  26206  dchrabs2  26398  dchr1re  26399  lgsneg1  26458  lgsdirprm  26467  lgsdir  26468  lgsne0  26471  lgsdirnn0  26480  lgsdinn0  26481  2sqlem9  26563  rpvmasumlem  26623  dchrvmasumiflem1  26637  dchrisum0flblem1  26644  rpvmasum2  26648  pntrsumbnd2  26703  pntleml  26747  tgcgrextend  26834  tgbtwnexch2  26845  tgifscgr  26857  tgcolg  26903  tgidinside  26920  tgbtwnconn1lem2  26922  tgbtwnconn1lem3  26923  lnhl  26964  tglinethru  26985  tglnpt2  26990  tglineneq  26993  coltr  26996  coltr3  26997  colline  26998  mirreu3  27003  miriso  27019  mirln  27025  mirln2  27026  mirconn  27027  mirbtwnhl  27029  colmid  27037  krippenlem  27039  midexlem  27041  ragflat  27053  ragcgr  27056  perprag  27075  perpdragALT  27076  colperpexlem1  27079  colperpexlem3  27081  midex  27086  opphllem1  27096  opphllem2  27097  opphllem5  27100  opphllem6  27101  hlpasch  27105  lmiisolem  27145  hypcgrlem1  27148  hypcgrlem2  27149  cgrg3col4  27202  upgrex  27450  crctcshwlk  28173  crctcsh  28175  1wlkdlem2  28488  eupth2lem3lem3  28580  eupth2lem3lem7  28584  nmcoplbi  30376  nmophmi  30379  nmbdfnlbi  30397  disjdifprg  30900  imadifxp  30926  2ndimaxp  30970  xlt2addrd  31067  ssnnssfz  31094  gsumpart  31301  symgcntz  31340  pmtridf1o  31347  pmtridfv1  31348  pmtridfv2  31349  psgnfzto1stlem  31353  tocycf  31370  cycpmco2lem5  31383  cycpmco2  31386  linds2eq  31561  locfinref  31777  zarcmplem  31817  esumpr2  32021  unelldsys  32112  sigapildsyslem  32115  sigapildsys  32116  mbfmcst  32212  carsgsigalem  32268  carsgclctunlem3  32273  pmeasmono  32277  probun  32372  0rrv  32404  sgncl  32491  signsvtn0  32535  signstfvneq0  32537  fineqvac  33052  frxp2  33777  frxp3  33783  btwnconn1lem11  34385  finxp00  35559  matunitlindf  35761  poimirlem14  35777  mblfinlem1  35800  mblfinlem2  35801  ismblfin  35804  itg2addnclem  35814  itgaddnclem2  35822  areacirclem4  35854  areacirc  35856  isbnd3  35928  blbnd  35931  rrnequiv  35979  lsmsat  37008  lkrscss  37098  eqlkr  37099  lkrshpor  37107  atcvrj2b  37432  atltcvr  37435  3dim1  37467  3dim2  37468  3dim3  37469  ps-2  37478  2at0mat0  37525  dalemdnee  37666  dalem63  37735  lnatexN  37779  2llnma3r  37788  pmodlem1  37846  pmapjat1  37853  pclfinclN  37950  osumclN  37967  pexmidALTN  37978  lhpexle2lem  38009  lhpexle3lem  38011  4atexlemex6  38074  4atex  38076  trlnle  38186  trlval3  38187  cdlemc  38197  cdlemd9  38206  cdleme27N  38369  cdleme28c  38372  cdleme32fvaw  38439  cdleme42ke  38485  cdleme42keg  38486  cdleme42mgN  38488  cdleme17d  38498  cdleme48fvg  38500  cdleme50trn123  38554  cdlemb3  38606  cdlemg8  38631  cdlemg15a  38655  cdlemg15  38656  cdlemg16  38657  cdlemg16ALTN  38658  cdlemg16z  38659  cdlemg16zz  38660  cdlemg20  38685  cdlemg22  38687  cdlemg37  38689  cdlemg31d  38700  cdlemg39  38716  cdlemg40  38717  ltrncom  38738  tendotr  38830  cdlemk25-3  38904  cdlemk35s-id  38938  cdlemk39s-id  38940  cdlemk53b  38956  cdlemk53  38957  cdlemk55  38961  cdlemk35u  38964  cdlemk55u  38966  cdlemk39u  38968  cdlemk19u  38970  cdleml5N  38980  dia2dimlem7  39070  dia2dimlem13  39076  dih1dimatlem  39329  dihlsprn  39331  dihjat1lem  39428  dihjat1  39429  dvh2dim  39445  dochexmid  39468  lclkrlem1  39506  lclkrlem2i  39515  lclkrlem2t  39526  lcfrlem34  39576  lcfrlem38  39580  lcfrlem41  39583  mapdindp1  39720  mapdindp2  39721  mapdh6dN  39739  mapdh6jN  39745  mapdh8j  39787  mapdh8  39788  hdmap1l6d  39813  hdmap1l6j  39819  hdmap11lem2  39842  hdmap14lem7  39874  jm2.19  40801  jm2.23  40804  nzss  41894  disjxp1  42576  cnrefiisplem  43329  xlimliminflimsup  43362  stoweidlem58  43558  fourierdlem41  43648  fourierdlem48  43654  fouriersw  43731  etransclem24  43758  nnfoctbdjlem  43952  ssnn0ssfz  45641  mreclat  46239