Theorem pm2.61dane 3019

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

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

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 2933

This theorem is referenced by:  pm2.61da2ne  3020  pm2.61da3ne  3021  pm2.61iine  3022  disjxiun  5095  onfr  6356  f1oprswap  6819  soex  7863  frxp2  8086  frxp3  8093  riiner  8727  difsnen  8987  mapdom2  9076  nnunifi  9191  fofinf1o  9232  brwdom2  9478  cantnff  9583  cantnfp1  9590  carddomi2  9882  wdomfil  9971  fin1a2lem10  10319  fin1a2lem11  10320  uzsupss  12853  xaddcom  13155  xnegdi  13163  xpncan  13166  xleadd1a  13168  xsubge0  13176  ccat1st1st  14552  swrdccatin1  14648  cnpart  15163  fsumcllem  15655  fsumrev2  15705  expcnv  15787  geomulcvg  15799  fprodcllem  15874  fsumdvds  16235  gcd0id  16446  nn0seqcvgd  16497  lcmdvds  16535  mulgcddvds  16582  pcge0  16790  pcneg  16802  pcdvdstr  16804  pcz  16809  pcprmpw2  16810  pcadd  16817  ramcl2  16944  0ramcl  16951  ramub1lem1  16954  ramcl  16957  mrerintcl  17516  mreriincl  17517  mreexexlem4d  17570  mreclatBAD  18486  chnub  18545  psgnunilem1  19422  odmulg  19485  sylow1lem1  19527  pgpfi  19534  odadd1  19777  odadd2  19778  gsumval3  19836  gsumpt  19891  dprdfcntz  19946  dprd2da  19973  ablfac1eulem  20003  pgpfaclem3  20014  ablsimpgfind  20041  abvneg  20759  lssssr  20905  lspsneq  21077  lspdisj2  21082  drngnidl  21198  cnsubrg  21382  riinopn  22852  riincld  22988  neipeltop  23073  hauscmplem  23350  cmpfi  23352  ptbasfi  23525  xkoccn  23563  txindislem  23577  txtube  23584  hmphindis  23741  fclscmp  23974  utop2nei  24194  nrginvrcn  24636  nmoleub  24675  blcvx  24742  xrsxmet  24754  xrsblre  24756  lebnumlem3  24918  cphsqrtcl2  25142  ovollb2  25446  ioorcl  25534  i1fmulc  25660  itg1mulc  25661  mbfi1fseqlem4  25675  bddiblnc  25799  dvlip  25954  dvne0  25972  ig1pdvds  26141  plyeq0lem  26171  plyeq0  26172  aannenlem2  26293  aalioulem6  26301  abelthlem8  26405  abelth  26407  cxpexp  26633  cxpge0  26648  cxpmul2  26654  abscxp2  26658  abscxpbnd  26719  cxpeq  26723  nnlogbexp  26747  isosctrlem2  26785  atanrecl  26877  wilthlem2  27035  dchrabs2  27229  dchr1re  27230  lgsneg1  27289  lgsdirprm  27298  lgsdir  27299  lgsne0  27302  lgsdirnn0  27311  lgsdinn0  27312  2sqlem9  27394  rpvmasumlem  27454  dchrvmasumiflem1  27468  dchrisum0flblem1  27475  rpvmasum2  27479  pntrsumbnd2  27534  pntleml  27578  tgcgrextend  28557  tgbtwnexch2  28568  tgifscgr  28580  tgcolg  28626  tgidinside  28643  tgbtwnconn1lem2  28645  tgbtwnconn1lem3  28646  lnhl  28687  tglinethru  28708  tglnpt2  28713  tglineneq  28716  coltr  28719  coltr3  28720  colline  28721  mirreu3  28726  miriso  28742  mirln  28748  mirln2  28749  mirconn  28750  mirbtwnhl  28752  colmid  28760  krippenlem  28762  midexlem  28764  ragflat  28776  ragcgr  28779  perprag  28798  perpdragALT  28799  colperpexlem1  28802  colperpexlem3  28804  midex  28809  opphllem1  28819  opphllem2  28820  opphllem5  28823  opphllem6  28824  hlpasch  28828  lmiisolem  28868  hypcgrlem1  28871  hypcgrlem2  28872  cgrg3col4  28925  upgrex  29165  crctcshwlk  29895  crctcsh  29897  1wlkdlem2  30213  eupth2lem3lem3  30305  eupth2lem3lem7  30309  nmcoplbi  32103  nmophmi  32106  nmbdfnlbi  32124  disjdifprg  32650  imadifxp  32676  2ndimaxp  32724  mptiffisupp  32772  xlt2addrd  32839  ssnnssfz  32867  sgncl  32912  gsumpart  33146  symgcntz  33167  fzo0pmtrlast  33174  pmtridf1o  33176  pmtridfv1  33177  pmtridfv2  33178  psgnfzto1stlem  33182  tocycf  33199  cycpmco2lem5  33212  cycpmco2  33215  fxpgaval  33249  linds2eq  33462  dvdsruasso  33466  ply1coedeg  33670  ply1degltel  33675  ply1degleel  33676  ig1pmindeg  33683  esplyind  33731  fldext2chn  33885  constraddcl  33919  constrremulcl  33924  constrsqrtcl  33936  cos9thpiminplylem2  33940  locfinref  33998  zarcmplem  34038  esumpr2  34224  unelldsys  34315  sigapildsyslem  34318  sigapildsys  34319  mbfmcst  34416  carsgsigalem  34472  carsgclctunlem3  34477  pmeasmono  34481  probun  34576  0rrv  34608  signsvtn0  34727  signstfvneq0  34729  fineqvac  35272  wevgblacfn  35303  btwnconn1lem11  36291  finxp00  37603  matunitlindf  37815  poimirlem14  37831  mblfinlem1  37854  mblfinlem2  37855  ismblfin  37858  itg2addnclem  37868  itgaddnclem2  37876  areacirclem4  37908  areacirc  37910  isbnd3  37981  blbnd  37984  rrnequiv  38032  lsmsat  39264  lkrscss  39354  eqlkr  39355  lkrshpor  39363  atcvrj2b  39688  atltcvr  39691  3dim1  39723  3dim2  39724  3dim3  39725  ps-2  39734  2at0mat0  39781  dalemdnee  39922  dalem63  39991  lnatexN  40035  2llnma3r  40044  pmodlem1  40102  pmapjat1  40109  pclfinclN  40206  osumclN  40223  pexmidALTN  40234  lhpexle2lem  40265  lhpexle3lem  40267  4atexlemex6  40330  4atex  40332  trlnle  40442  trlval3  40443  cdlemc  40453  cdlemd9  40462  cdleme27N  40625  cdleme28c  40628  cdleme32fvaw  40695  cdleme42ke  40741  cdleme42keg  40742  cdleme42mgN  40744  cdleme17d  40754  cdleme48fvg  40756  cdleme50trn123  40810  cdlemb3  40862  cdlemg8  40887  cdlemg15a  40911  cdlemg15  40912  cdlemg16  40913  cdlemg16ALTN  40914  cdlemg16z  40915  cdlemg16zz  40916  cdlemg20  40941  cdlemg22  40943  cdlemg37  40945  cdlemg31d  40956  cdlemg39  40972  cdlemg40  40973  ltrncom  40994  tendotr  41086  cdlemk25-3  41160  cdlemk35s-id  41194  cdlemk39s-id  41196  cdlemk53b  41212  cdlemk53  41213  cdlemk55  41217  cdlemk35u  41220  cdlemk55u  41222  cdlemk39u  41224  cdlemk19u  41226  cdleml5N  41236  dia2dimlem7  41326  dia2dimlem13  41332  dih1dimatlem  41585  dihlsprn  41587  dihjat1lem  41684  dihjat1  41685  dvh2dim  41701  dochexmid  41724  lclkrlem1  41762  lclkrlem2i  41771  lclkrlem2t  41782  lcfrlem34  41832  lcfrlem38  41836  lcfrlem41  41839  mapdindp1  41976  mapdindp2  41977  mapdh6dN  41995  mapdh6jN  42001  mapdh8j  42043  mapdh8  42044  hdmap1l6d  42069  hdmap1l6j  42075  hdmap11lem2  42098  hdmap14lem7  42130  primrootlekpowne0  42355  aks6d1c7lem2  42431  unitscyglem4  42448  jm2.19  43231  jm2.23  43234  nzss  44554  disjxp1  45310  cnrefiisplem  46069  xlimliminflimsup  46102  stoweidlem58  46298  fourierdlem41  46388  fourierdlem48  46394  fouriersw  46471  etransclem24  46498  nnfoctbdjlem  46695  smfpimltxr  46987  smfpimgtxr  47020  chnerlem1  47122  ssnn0ssfz  48591  mreclat  49238