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  5097  onfr  6364  f1oprswap  6827  soex  7873  frxp2  8096  frxp3  8103  riiner  8739  difsnen  8999  mapdom2  9088  nnunifi  9203  fofinf1o  9244  brwdom2  9490  cantnff  9595  cantnfp1  9602  carddomi2  9894  wdomfil  9983  fin1a2lem10  10331  fin1a2lem11  10332  uzsupss  12865  xaddcom  13167  xnegdi  13175  xpncan  13178  xleadd1a  13180  xsubge0  13188  ccat1st1st  14564  swrdccatin1  14660  cnpart  15175  fsumcllem  15667  fsumrev2  15717  expcnv  15799  geomulcvg  15811  fprodcllem  15886  fsumdvds  16247  gcd0id  16458  nn0seqcvgd  16509  lcmdvds  16547  mulgcddvds  16594  pcge0  16802  pcneg  16814  pcdvdstr  16816  pcz  16821  pcprmpw2  16822  pcadd  16829  ramcl2  16956  0ramcl  16963  ramub1lem1  16966  ramcl  16969  mrerintcl  17528  mreriincl  17529  mreexexlem4d  17582  mreclatBAD  18498  chnub  18557  psgnunilem1  19434  odmulg  19497  sylow1lem1  19539  pgpfi  19546  odadd1  19789  odadd2  19790  gsumval3  19848  gsumpt  19903  dprdfcntz  19958  dprd2da  19985  ablfac1eulem  20015  pgpfaclem3  20026  ablsimpgfind  20053  abvneg  20771  lssssr  20917  lspsneq  21089  lspdisj2  21094  drngnidl  21210  cnsubrg  21394  riinopn  22864  riincld  23000  neipeltop  23085  hauscmplem  23362  cmpfi  23364  ptbasfi  23537  xkoccn  23575  txindislem  23589  txtube  23596  hmphindis  23753  fclscmp  23986  utop2nei  24206  nrginvrcn  24648  nmoleub  24687  blcvx  24754  xrsxmet  24766  xrsblre  24768  lebnumlem3  24930  cphsqrtcl2  25154  ovollb2  25458  ioorcl  25546  i1fmulc  25672  itg1mulc  25673  mbfi1fseqlem4  25687  bddiblnc  25811  dvlip  25966  dvne0  25984  ig1pdvds  26153  plyeq0lem  26183  plyeq0  26184  aannenlem2  26305  aalioulem6  26313  abelthlem8  26417  abelth  26419  cxpexp  26645  cxpge0  26660  cxpmul2  26666  abscxp2  26670  abscxpbnd  26731  cxpeq  26735  nnlogbexp  26759  isosctrlem2  26797  atanrecl  26889  wilthlem2  27047  dchrabs2  27241  dchr1re  27242  lgsneg1  27301  lgsdirprm  27310  lgsdir  27311  lgsne0  27314  lgsdirnn0  27323  lgsdinn0  27324  2sqlem9  27406  rpvmasumlem  27466  dchrvmasumiflem1  27480  dchrisum0flblem1  27487  rpvmasum2  27491  pntrsumbnd2  27546  pntleml  27590  tgcgrextend  28569  tgbtwnexch2  28580  tgifscgr  28592  tgcolg  28638  tgidinside  28655  tgbtwnconn1lem2  28657  tgbtwnconn1lem3  28658  lnhl  28699  tglinethru  28720  tglnpt2  28725  tglineneq  28728  coltr  28731  coltr3  28732  colline  28733  mirreu3  28738  miriso  28754  mirln  28760  mirln2  28761  mirconn  28762  mirbtwnhl  28764  colmid  28772  krippenlem  28774  midexlem  28776  ragflat  28788  ragcgr  28791  perprag  28810  perpdragALT  28811  colperpexlem1  28814  colperpexlem3  28816  midex  28821  opphllem1  28831  opphllem2  28832  opphllem5  28835  opphllem6  28836  hlpasch  28840  lmiisolem  28880  hypcgrlem1  28883  hypcgrlem2  28884  cgrg3col4  28937  upgrex  29177  crctcshwlk  29907  crctcsh  29909  1wlkdlem2  30225  eupth2lem3lem3  30317  eupth2lem3lem7  30321  nmcoplbi  32115  nmophmi  32118  nmbdfnlbi  32136  disjdifprg  32661  imadifxp  32687  2ndimaxp  32735  mptiffisupp  32782  xlt2addrd  32849  ssnnssfz  32877  sgncl  32922  gsumpart  33156  suppgsumssiun  33165  symgcntz  33178  fzo0pmtrlast  33185  pmtridf1o  33187  pmtridfv1  33188  pmtridfv2  33189  psgnfzto1stlem  33193  tocycf  33210  cycpmco2lem5  33223  cycpmco2  33226  fxpgaval  33260  linds2eq  33473  dvdsruasso  33477  ply1coedeg  33681  ply1degltel  33686  ply1degleel  33687  ig1pmindeg  33694  esplyind  33751  fldext2chn  33905  constraddcl  33939  constrremulcl  33944  constrsqrtcl  33956  cos9thpiminplylem2  33960  locfinref  34018  zarcmplem  34058  esumpr2  34244  unelldsys  34335  sigapildsyslem  34338  sigapildsys  34339  mbfmcst  34436  carsgsigalem  34492  carsgclctunlem3  34497  pmeasmono  34501  probun  34596  0rrv  34628  signsvtn0  34747  signstfvneq0  34749  fineqvac  35291  wevgblacfn  35322  btwnconn1lem11  36310  finxp00  37651  matunitlindf  37863  poimirlem14  37879  mblfinlem1  37902  mblfinlem2  37903  ismblfin  37906  itg2addnclem  37916  itgaddnclem2  37924  areacirclem4  37956  areacirc  37958  isbnd3  38029  blbnd  38032  rrnequiv  38080  lsmsat  39378  lkrscss  39468  eqlkr  39469  lkrshpor  39477  atcvrj2b  39802  atltcvr  39805  3dim1  39837  3dim2  39838  3dim3  39839  ps-2  39848  2at0mat0  39895  dalemdnee  40036  dalem63  40105  lnatexN  40149  2llnma3r  40158  pmodlem1  40216  pmapjat1  40223  pclfinclN  40320  osumclN  40337  pexmidALTN  40348  lhpexle2lem  40379  lhpexle3lem  40381  4atexlemex6  40444  4atex  40446  trlnle  40556  trlval3  40557  cdlemc  40567  cdlemd9  40576  cdleme27N  40739  cdleme28c  40742  cdleme32fvaw  40809  cdleme42ke  40855  cdleme42keg  40856  cdleme42mgN  40858  cdleme17d  40868  cdleme48fvg  40870  cdleme50trn123  40924  cdlemb3  40976  cdlemg8  41001  cdlemg15a  41025  cdlemg15  41026  cdlemg16  41027  cdlemg16ALTN  41028  cdlemg16z  41029  cdlemg16zz  41030  cdlemg20  41055  cdlemg22  41057  cdlemg37  41059  cdlemg31d  41070  cdlemg39  41086  cdlemg40  41087  ltrncom  41108  tendotr  41200  cdlemk25-3  41274  cdlemk35s-id  41308  cdlemk39s-id  41310  cdlemk53b  41326  cdlemk53  41327  cdlemk55  41331  cdlemk35u  41334  cdlemk55u  41336  cdlemk39u  41338  cdlemk19u  41340  cdleml5N  41350  dia2dimlem7  41440  dia2dimlem13  41446  dih1dimatlem  41699  dihlsprn  41701  dihjat1lem  41798  dihjat1  41799  dvh2dim  41815  dochexmid  41838  lclkrlem1  41876  lclkrlem2i  41885  lclkrlem2t  41896  lcfrlem34  41946  lcfrlem38  41950  lcfrlem41  41953  mapdindp1  42090  mapdindp2  42091  mapdh6dN  42109  mapdh6jN  42115  mapdh8j  42157  mapdh8  42158  hdmap1l6d  42183  hdmap1l6j  42189  hdmap11lem2  42212  hdmap14lem7  42244  primrootlekpowne0  42469  aks6d1c7lem2  42545  unitscyglem4  42562  jm2.19  43344  jm2.23  43347  nzss  44667  disjxp1  45423  cnrefiisplem  46181  xlimliminflimsup  46214  stoweidlem58  46410  fourierdlem41  46500  fourierdlem48  46506  fouriersw  46583  etransclem24  46610  nnfoctbdjlem  46807  smfpimltxr  47099  smfpimgtxr  47132  chnerlem1  47234  ssnn0ssfz  48703  mreclat  49350