Theorem pm2.61dane 3045

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ≠ wne 2958

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 2959

This theorem is referenced by:  pm2.61da2ne  3046  pm2.61da3ne  3047  pm2.61iine  3048  disjxiun  5107  onfr  6402  f1oprswap  6868  soex  7919  frxp2  8141  frxp3  8148  riiner  8789  difsnen  9048  mapdom2  9137  nnunifi  9252  fofinf1o  9290  brwdom2  9536  cantnff  9644  cantnfp1  9651  carddomi2  9957  wdomfil  10046  fin1a2lem10  10394  fin1a2lem11  10395  uzsupss  12965  xaddcom  13267  xnegdi  13275  xpncan  13278  xleadd1a  13280  xsubge0  13288  ccat1st1st  14668  swrdccatin1  14764  sgncl  15136  cnpart  15293  fsumcllem  15785  fsumrev2  15835  expcnv  15920  geomulcvg  15932  fprodcllem  16007  fsumdvds  16367  gcd0id  16578  nn0seqcvgd  16629  lcmdvds  16667  mulgcddvds  16714  pcge0  16923  pcneg  16935  pcdvdstr  16937  pcz  16942  pcprmpw2  16943  pcadd  16950  ramcl2  17077  0ramcl  17084  ramub1lem1  17087  ramcl  17090  mrerintcl  17650  mreriincl  17651  mreexexlem4d  17704  mreclatBAD  18620  chnub  18679  psgnunilem1  19564  odmulg  19627  sylow1lem1  19669  pgpfi  19676  odadd1  19919  odadd2  19920  gsumval3  19978  gsumpt  20033  dprdfcntz  20088  dprd2da  20115  ablfac1eulem  20145  pgpfaclem3  20156  ablsimpgfind  20183  abvneg  20910  lssssr  21056  lspsneq  21227  lspdisj2  21232  drngnidl  21358  cnsubrg  21558  riinopn  23046  riincld  23182  neipeltop  23267  hauscmplem  23544  cmpfi  23546  ptbasfi  23719  xkoccn  23757  txindislem  23771  txtube  23778  hmphindis  23935  fclscmp  24168  utop2nei  24388  nrginvrcn  24830  nmoleub  24869  blcvx  24936  xrsxmet  24948  xrsblre  24950  lebnumlem3  25103  cphsqrtcl2  25326  ovollb2  25629  ioorcl  25717  i1fmulc  25843  itg1mulc  25844  mbfi1fseqlem4  25858  bddiblnc  25982  dvlip  26133  dvne0  26151  ig1pdvds  26318  plyeq0lem  26348  plyeq0  26349  aannenlem2  26473  aalioulem6  26481  abelthlem8  26583  abelth  26585  cxpexp  26814  cxpge0  26829  cxpmul2  26835  abscxp2  26839  abscxpbnd  26899  cxpeq  26903  nnlogbexp  26927  isosctrlem2  26965  atanrecl  27057  wilthlem2  27214  dchrabs2  27407  dchr1re  27408  lgsneg1  27467  lgsdirprm  27476  lgsdir  27477  lgsne0  27480  lgsdirnn0  27489  lgsdinn0  27490  2sqlem9  27572  rpvmasumlem  27632  dchrvmasumiflem1  27646  dchrisum0flblem1  27653  rpvmasum2  27657  pntrsumbnd2  27712  pntleml  27756  tgcgrextend  28735  tgbtwnexch2  28746  tgifscgr  28758  tgcolg  28804  tgidinside  28821  tgbtwnconn1lem2  28823  tgbtwnconn1lem3  28824  lnhl  28868  tglinethru  28890  tglineneq  28899  coltr  28902  coltr3  28903  colline  28904  tglnpt2  28907  tglnpt4  28909  mirreu3  28912  miriso  28928  mirln  28934  mirln2  28935  mirconn  28936  mirbtwnhl  28938  colmid  28946  krippenlem  28948  midexlem  28950  ragflat  28965  ragcgr  28968  perprag  28988  perpdragALT  28989  colperpexlem1  28992  colperpexlem3  28994  midex  28999  opphllem1  29009  opphllem2  29010  opphllem5  29013  opphllem6  29014  hlpasch  29019  lnincplng  29047  lnssplng  29055  mirplncl  29058  lmiisolem  29086  hypcgrlem1  29090  hypcgrlem2  29091  cgrg3col4  29151  prlnghpg  29177  perpprlng  29181  prlngmolem2  29184  prlngpln4  29189  prlngplngtr  29190  prlngmid2  29192  upgrex  29423  crctcshwlk  30152  crctcsh  30154  1wlkdlem2  30470  eupth2lem3lem3  30562  eupth2lem3lem7  30566  nmcoplbi  32361  nmophmi  32364  nmbdfnlbi  32382  disjdifprg  32901  imadifxp  32927  2ndimaxp  32972  mptiffisupp  33019  xlt2addrd  33085  ssnnssfz  33113  gsumpart  33364  suppgsumssiun  33373  symgcntz  33386  fzo0pmtrlast  33393  pmtridf1o  33395  pmtridfv1  33396  pmtridfv2  33397  psgnfzto1stlem  33401  tocycf  33418  cycpmco2lem5  33431  cycpmco2  33434  fxpgaval  33468  linds2eq  33675  dvdsruasso  33679  ply1coedeg  33860  ply1degltel  33865  ply1degleel  33866  ig1pmindeg  33873  esplyind  33946  fldext2chn  34099  constraddcl  34133  constrremulcl  34138  constrsqrtcl  34150  cos9thpiminplylem2  34154  locfinref  34212  zarcmplem  34252  esumpr2  34438  unelldsys  34529  sigapildsyslem  34532  sigapildsys  34533  mbfmcst  34630  carsgsigalem  34686  carsgclctunlem3  34691  pmeasmono  34695  probun  34790  0rrv  34822  signsvtn0  34938  signstfvneq0  34940  fineqvac  35510  wevgblacfn  35576  btwnconn1lem11  36570  finxp00  38029  matunitlindf  38250  poimirlem14  38266  mblfinlem1  38289  mblfinlem2  38290  ismblfin  38293  itg2addnclem  38303  itgaddnclem2  38311  areacirclem4  38343  areacirc  38345  isbnd3  38416  blbnd  38419  rrnequiv  38467  lsmsat  39763  lkrscss  39853  eqlkr  39854  lkrshpor  39862  atcvrj2b  40187  atltcvr  40190  3dim1  40222  3dim2  40223  3dim3  40224  ps-2  40233  2at0mat0  40280  dalemdnee  40421  dalem63  40490  lnatexN  40534  2llnma3r  40543  pmodlem1  40601  pmapjat1  40608  pclfinclN  40705  osumclN  40722  pexmidALTN  40733  lhpexle2lem  40764  lhpexle3lem  40766  4atexlemex6  40829  4atex  40831  trlnle  40941  trlval3  40942  cdlemc  40952  cdlemd9  40961  cdleme27N  41124  cdleme28c  41127  cdleme32fvaw  41194  cdleme42ke  41240  cdleme42keg  41241  cdleme42mgN  41243  cdleme17d  41253  cdleme48fvg  41255  cdleme50trn123  41309  cdlemb3  41361  cdlemg8  41386  cdlemg15a  41410  cdlemg15  41411  cdlemg16  41412  cdlemg16ALTN  41413  cdlemg16z  41414  cdlemg16zz  41415  cdlemg20  41440  cdlemg22  41442  cdlemg37  41444  cdlemg31d  41455  cdlemg39  41471  cdlemg40  41472  ltrncom  41493  tendotr  41585  cdlemk25-3  41659  cdlemk35s-id  41693  cdlemk39s-id  41695  cdlemk53b  41711  cdlemk53  41712  cdlemk55  41716  cdlemk35u  41719  cdlemk55u  41721  cdlemk39u  41723  cdlemk19u  41725  cdleml5N  41735  dia2dimlem7  41825  dia2dimlem13  41831  dih1dimatlem  42084  dihlsprn  42086  dihjat1lem  42183  dihjat1  42184  dvh2dim  42200  dochexmid  42223  lclkrlem1  42261  lclkrlem2i  42270  lclkrlem2t  42281  lcfrlem34  42331  lcfrlem38  42335  lcfrlem41  42338  mapdindp1  42475  mapdindp2  42476  mapdh6dN  42494  mapdh6jN  42500  mapdh8j  42542  mapdh8  42543  hdmap1l6d  42568  hdmap1l6j  42574  hdmap11lem2  42597  hdmap14lem7  42629  primrootlekpowne0  42853  aks6d1c7lem2  42929  unitscyglem4  42946  jm2.19  43703  jm2.23  43706  nzss  45010  disjxp1  45772  cnrefiisplem  46526  xlimliminflimsup  46559  stoweidlem58  46755  fourierdlem41  46845  fourierdlem48  46851  fouriersw  46928  etransclem24  46955  nnfoctbdjlem  47152  smfpimltxr  47444  smfpimgtxr  47477  chnerlem1  47581  sqrtqaa  47589  ssnn0ssfz  49112  mreclat  49758