Theorem pm2.61dane 3013

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ≠ wne 2926

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 2927

This theorem is referenced by:  pm2.61da2ne  3014  pm2.61da3ne  3015  pm2.61iine  3016  disjxiun  5107  onfr  6374  f1oprswap  6847  soex  7900  frxp2  8126  frxp3  8133  riiner  8766  difsnen  9027  mapdom2  9118  nnunifi  9245  fofinf1o  9290  brwdom2  9533  cantnff  9634  cantnfp1  9641  carddomi2  9930  wdomfil  10021  fin1a2lem10  10369  fin1a2lem11  10370  uzsupss  12906  xaddcom  13207  xnegdi  13215  xpncan  13218  xleadd1a  13220  xsubge0  13228  ccat1st1st  14600  swrdccatin1  14697  cnpart  15213  fsumcllem  15705  fsumrev2  15755  expcnv  15837  geomulcvg  15849  fprodcllem  15924  fsumdvds  16285  gcd0id  16496  nn0seqcvgd  16547  lcmdvds  16585  mulgcddvds  16632  pcge0  16840  pcneg  16852  pcdvdstr  16854  pcz  16859  pcprmpw2  16860  pcadd  16867  ramcl2  16994  0ramcl  17001  ramub1lem1  17004  ramcl  17007  mrerintcl  17565  mreriincl  17566  mreexexlem4d  17615  mreclatBAD  18529  psgnunilem1  19430  odmulg  19493  sylow1lem1  19535  pgpfi  19542  odadd1  19785  odadd2  19786  gsumval3  19844  gsumpt  19899  dprdfcntz  19954  dprd2da  19981  ablfac1eulem  20011  pgpfaclem3  20022  ablsimpgfind  20049  abvneg  20742  lssssr  20867  lspsneq  21039  lspdisj2  21044  drngnidl  21160  cnsubrg  21351  riinopn  22802  riincld  22938  neipeltop  23023  hauscmplem  23300  cmpfi  23302  ptbasfi  23475  xkoccn  23513  txindislem  23527  txtube  23534  hmphindis  23691  fclscmp  23924  utop2nei  24145  nrginvrcn  24587  nmoleub  24626  blcvx  24693  xrsxmet  24705  xrsblre  24707  lebnumlem3  24869  cphsqrtcl2  25093  ovollb2  25397  ioorcl  25485  i1fmulc  25611  itg1mulc  25612  mbfi1fseqlem4  25626  bddiblnc  25750  dvlip  25905  dvne0  25923  ig1pdvds  26092  plyeq0lem  26122  plyeq0  26123  aannenlem2  26244  aalioulem6  26252  abelthlem8  26356  abelth  26358  cxpexp  26584  cxpge0  26599  cxpmul2  26605  abscxp2  26609  abscxpbnd  26670  cxpeq  26674  nnlogbexp  26698  isosctrlem2  26736  atanrecl  26828  wilthlem2  26986  dchrabs2  27180  dchr1re  27181  lgsneg1  27240  lgsdirprm  27249  lgsdir  27250  lgsne0  27253  lgsdirnn0  27262  lgsdinn0  27263  2sqlem9  27345  rpvmasumlem  27405  dchrvmasumiflem1  27419  dchrisum0flblem1  27426  rpvmasum2  27430  pntrsumbnd2  27485  pntleml  27529  tgcgrextend  28419  tgbtwnexch2  28430  tgifscgr  28442  tgcolg  28488  tgidinside  28505  tgbtwnconn1lem2  28507  tgbtwnconn1lem3  28508  lnhl  28549  tglinethru  28570  tglnpt2  28575  tglineneq  28578  coltr  28581  coltr3  28582  colline  28583  mirreu3  28588  miriso  28604  mirln  28610  mirln2  28611  mirconn  28612  mirbtwnhl  28614  colmid  28622  krippenlem  28624  midexlem  28626  ragflat  28638  ragcgr  28641  perprag  28660  perpdragALT  28661  colperpexlem1  28664  colperpexlem3  28666  midex  28671  opphllem1  28681  opphllem2  28682  opphllem5  28685  opphllem6  28686  hlpasch  28690  lmiisolem  28730  hypcgrlem1  28733  hypcgrlem2  28734  cgrg3col4  28787  upgrex  29026  crctcshwlk  29759  crctcsh  29761  1wlkdlem2  30074  eupth2lem3lem3  30166  eupth2lem3lem7  30170  nmcoplbi  31964  nmophmi  31967  nmbdfnlbi  31985  disjdifprg  32511  imadifxp  32537  2ndimaxp  32577  mptiffisupp  32623  xlt2addrd  32689  ssnnssfz  32717  sgncl  32763  chnub  32945  gsumpart  33004  symgcntz  33049  fzo0pmtrlast  33056  pmtridf1o  33058  pmtridfv1  33059  pmtridfv2  33060  psgnfzto1stlem  33064  tocycf  33081  cycpmco2lem5  33094  cycpmco2  33097  fxpgaval  33131  linds2eq  33359  dvdsruasso  33363  ply1degltel  33567  ply1degleel  33568  ig1pmindeg  33574  fldext2chn  33725  constraddcl  33759  constrremulcl  33764  constrsqrtcl  33776  cos9thpiminplylem2  33780  locfinref  33838  zarcmplem  33878  esumpr2  34064  unelldsys  34155  sigapildsyslem  34158  sigapildsys  34159  mbfmcst  34257  carsgsigalem  34313  carsgclctunlem3  34318  pmeasmono  34322  probun  34417  0rrv  34449  signsvtn0  34568  signstfvneq0  34570  fineqvac  35094  wevgblacfn  35103  btwnconn1lem11  36092  finxp00  37397  matunitlindf  37619  poimirlem14  37635  mblfinlem1  37658  mblfinlem2  37659  ismblfin  37662  itg2addnclem  37672  itgaddnclem2  37680  areacirclem4  37712  areacirc  37714  isbnd3  37785  blbnd  37788  rrnequiv  37836  lsmsat  39008  lkrscss  39098  eqlkr  39099  lkrshpor  39107  atcvrj2b  39433  atltcvr  39436  3dim1  39468  3dim2  39469  3dim3  39470  ps-2  39479  2at0mat0  39526  dalemdnee  39667  dalem63  39736  lnatexN  39780  2llnma3r  39789  pmodlem1  39847  pmapjat1  39854  pclfinclN  39951  osumclN  39968  pexmidALTN  39979  lhpexle2lem  40010  lhpexle3lem  40012  4atexlemex6  40075  4atex  40077  trlnle  40187  trlval3  40188  cdlemc  40198  cdlemd9  40207  cdleme27N  40370  cdleme28c  40373  cdleme32fvaw  40440  cdleme42ke  40486  cdleme42keg  40487  cdleme42mgN  40489  cdleme17d  40499  cdleme48fvg  40501  cdleme50trn123  40555  cdlemb3  40607  cdlemg8  40632  cdlemg15a  40656  cdlemg15  40657  cdlemg16  40658  cdlemg16ALTN  40659  cdlemg16z  40660  cdlemg16zz  40661  cdlemg20  40686  cdlemg22  40688  cdlemg37  40690  cdlemg31d  40701  cdlemg39  40717  cdlemg40  40718  ltrncom  40739  tendotr  40831  cdlemk25-3  40905  cdlemk35s-id  40939  cdlemk39s-id  40941  cdlemk53b  40957  cdlemk53  40958  cdlemk55  40962  cdlemk35u  40965  cdlemk55u  40967  cdlemk39u  40969  cdlemk19u  40971  cdleml5N  40981  dia2dimlem7  41071  dia2dimlem13  41077  dih1dimatlem  41330  dihlsprn  41332  dihjat1lem  41429  dihjat1  41430  dvh2dim  41446  dochexmid  41469  lclkrlem1  41507  lclkrlem2i  41516  lclkrlem2t  41527  lcfrlem34  41577  lcfrlem38  41581  lcfrlem41  41584  mapdindp1  41721  mapdindp2  41722  mapdh6dN  41740  mapdh6jN  41746  mapdh8j  41788  mapdh8  41789  hdmap1l6d  41814  hdmap1l6j  41820  hdmap11lem2  41843  hdmap14lem7  41875  primrootlekpowne0  42100  aks6d1c7lem2  42176  unitscyglem4  42193  jm2.19  42989  jm2.23  42992  nzss  44313  disjxp1  45070  cnrefiisplem  45834  xlimliminflimsup  45867  stoweidlem58  46063  fourierdlem41  46153  fourierdlem48  46159  fouriersw  46236  etransclem24  46263  nnfoctbdjlem  46460  smfpimltxr  46752  smfpimgtxr  46785  ssnn0ssfz  48341  mreclat  48989