Theorem pm2.61dane 3047

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ≠ wne 2960

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 210  df-an 401  df-ne 2961

This theorem is referenced by:  pm2.61da2ne  3048  pm2.61da3ne  3049  pm2.61iine  3050  disjxiun  5102  onfr  6389  f1oprswap  6856  soex  7906  frxp2  8128  frxp3  8135  riiner  8776  difsnen  9035  mapdom2  9124  nnunifi  9239  fofinf1o  9277  brwdom2  9523  cantnff  9631  cantnfp1  9638  carddomi2  9944  wdomfil  10033  fin1a2lem10  10381  fin1a2lem11  10382  uzsupss  12955  xaddcom  13257  xnegdi  13265  xpncan  13268  xleadd1a  13270  xsubge0  13278  ccat1st1st  14656  swrdccatin1  14752  sgncl  15124  cnpart  15281  fsumcllem  15773  fsumrev2  15823  expcnv  15908  geomulcvg  15920  fprodcllem  15995  fsumdvds  16356  gcd0id  16567  nn0seqcvgd  16618  lcmdvds  16656  mulgcddvds  16703  pcge0  16912  pcneg  16924  pcdvdstr  16926  pcz  16931  pcprmpw2  16932  pcadd  16939  ramcl2  17066  0ramcl  17073  ramub1lem1  17076  ramcl  17079  mrerintcl  17639  mreriincl  17640  mreexexlem4d  17693  mreclatBAD  18609  chnub  18668  psgnunilem1  19554  odmulg  19617  sylow1lem1  19659  pgpfi  19666  odadd1  19909  odadd2  19910  gsumval3  19968  gsumpt  20023  dprdfcntz  20078  dprd2da  20105  ablfac1eulem  20135  pgpfaclem3  20146  ablsimpgfind  20173  abvneg  20898  lssssr  21044  lspsneq  21215  lspdisj2  21220  drngnidl  21342  cnsubrg  21537  riinopn  23026  riincld  23162  neipeltop  23247  hauscmplem  23524  cmpfi  23526  ptbasfi  23699  xkoccn  23737  txindislem  23751  txtube  23758  hmphindis  23915  fclscmp  24148  utop2nei  24368  nrginvrcn  24810  nmoleub  24849  blcvx  24916  xrsxmet  24928  xrsblre  24930  lebnumlem3  25083  cphsqrtcl2  25306  ovollb2  25609  ioorcl  25697  i1fmulc  25823  itg1mulc  25824  mbfi1fseqlem4  25838  bddiblnc  25962  dvlip  26113  dvne0  26131  ig1pdvds  26298  plyeq0lem  26328  plyeq0  26329  aannenlem2  26451  aalioulem6  26459  abelthlem8  26560  abelth  26562  cxpexp  26791  cxpge0  26806  cxpmul2  26812  abscxp2  26816  abscxpbnd  26876  cxpeq  26880  nnlogbexp  26904  isosctrlem2  26942  atanrecl  27034  wilthlem2  27191  dchrabs2  27384  dchr1re  27385  lgsneg1  27444  lgsdirprm  27453  lgsdir  27454  lgsne0  27457  lgsdirnn0  27466  lgsdinn0  27467  2sqlem9  27549  rpvmasumlem  27609  dchrvmasumiflem1  27623  dchrisum0flblem1  27630  rpvmasum2  27634  pntrsumbnd2  27689  pntleml  27733  tgcgrextend  28712  tgbtwnexch2  28723  tgifscgr  28735  tgcolg  28781  tgidinside  28798  tgbtwnconn1lem2  28800  tgbtwnconn1lem3  28801  lnhl  28842  tglinethru  28863  tglineneq  28872  coltr  28875  coltr3  28876  colline  28877  tglnpt2  28880  tglnpt4  28882  mirreu3  28885  miriso  28901  mirln  28907  mirln2  28908  mirconn  28909  mirbtwnhl  28911  colmid  28919  krippenlem  28921  midexlem  28923  ragflat  28935  ragcgr  28938  perprag  28957  perpdragALT  28958  colperpexlem1  28961  colperpexlem3  28963  midex  28968  opphllem1  28978  opphllem2  28979  opphllem5  28982  opphllem6  28983  hlpasch  28987  lnincplng  29014  lnssplng  29022  lmiisolem  29048  hypcgrlem1  29051  hypcgrlem2  29052  cgrg3col4  29105  upgrex  29351  crctcshwlk  30080  crctcsh  30082  1wlkdlem2  30398  eupth2lem3lem3  30490  eupth2lem3lem7  30494  nmcoplbi  32289  nmophmi  32292  nmbdfnlbi  32310  disjdifprg  32830  imadifxp  32856  2ndimaxp  32903  mptiffisupp  32950  xlt2addrd  33016  ssnnssfz  33044  gsumpart  33296  suppgsumssiun  33305  symgcntz  33318  fzo0pmtrlast  33325  pmtridf1o  33327  pmtridfv1  33328  pmtridfv2  33329  psgnfzto1stlem  33333  tocycf  33350  cycpmco2lem5  33363  cycpmco2  33366  fxpgaval  33400  linds2eq  33610  dvdsruasso  33614  ply1coedeg  33796  ply1degltel  33801  ply1degleel  33802  ig1pmindeg  33809  esplyind  33882  fldext2chn  34035  constraddcl  34069  constrremulcl  34074  constrsqrtcl  34086  cos9thpiminplylem2  34090  locfinref  34148  zarcmplem  34188  esumpr2  34374  unelldsys  34465  sigapildsyslem  34468  sigapildsys  34469  mbfmcst  34566  carsgsigalem  34622  carsgclctunlem3  34627  pmeasmono  34631  probun  34726  0rrv  34758  signsvtn0  34874  signstfvneq0  34876  fineqvac  35424  wevgblacfn  35466  btwnconn1lem11  36460  finxp00  37908  matunitlindf  38129  poimirlem14  38145  mblfinlem1  38168  mblfinlem2  38169  ismblfin  38172  itg2addnclem  38182  itgaddnclem2  38190  areacirclem4  38222  areacirc  38224  isbnd3  38295  blbnd  38298  rrnequiv  38346  lsmsat  39644  lkrscss  39734  eqlkr  39735  lkrshpor  39743  atcvrj2b  40068  atltcvr  40071  3dim1  40103  3dim2  40104  3dim3  40105  ps-2  40114  2at0mat0  40161  dalemdnee  40302  dalem63  40371  lnatexN  40415  2llnma3r  40424  pmodlem1  40482  pmapjat1  40489  pclfinclN  40586  osumclN  40603  pexmidALTN  40614  lhpexle2lem  40645  lhpexle3lem  40647  4atexlemex6  40710  4atex  40712  trlnle  40822  trlval3  40823  cdlemc  40833  cdlemd9  40842  cdleme27N  41005  cdleme28c  41008  cdleme32fvaw  41075  cdleme42ke  41121  cdleme42keg  41122  cdleme42mgN  41124  cdleme17d  41134  cdleme48fvg  41136  cdleme50trn123  41190  cdlemb3  41242  cdlemg8  41267  cdlemg15a  41291  cdlemg15  41292  cdlemg16  41293  cdlemg16ALTN  41294  cdlemg16z  41295  cdlemg16zz  41296  cdlemg20  41321  cdlemg22  41323  cdlemg37  41325  cdlemg31d  41336  cdlemg39  41352  cdlemg40  41353  ltrncom  41374  tendotr  41466  cdlemk25-3  41540  cdlemk35s-id  41574  cdlemk39s-id  41576  cdlemk53b  41592  cdlemk53  41593  cdlemk55  41597  cdlemk35u  41600  cdlemk55u  41602  cdlemk39u  41604  cdlemk19u  41606  cdleml5N  41616  dia2dimlem7  41706  dia2dimlem13  41712  dih1dimatlem  41965  dihlsprn  41967  dihjat1lem  42064  dihjat1  42065  dvh2dim  42081  dochexmid  42104  lclkrlem1  42142  lclkrlem2i  42151  lclkrlem2t  42162  lcfrlem34  42212  lcfrlem38  42216  lcfrlem41  42219  mapdindp1  42356  mapdindp2  42357  mapdh6dN  42375  mapdh6jN  42381  mapdh8j  42423  mapdh8  42424  hdmap1l6d  42449  hdmap1l6j  42455  hdmap11lem2  42478  hdmap14lem7  42510  primrootlekpowne0  42734  aks6d1c7lem2  42810  unitscyglem4  42827  jm2.19  43582  jm2.23  43585  nzss  44891  disjxp1  45647  cnrefiisplem  46401  xlimliminflimsup  46434  stoweidlem58  46630  fourierdlem41  46720  fourierdlem48  46726  fouriersw  46803  etransclem24  46830  nnfoctbdjlem  47027  smfpimltxr  47319  smfpimgtxr  47352  chnerlem1  47456  ssnn0ssfz  48980  mreclat  49626