Theorem pm2.61dane 3035

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  pm2.61da2ne  3036  pm2.61da3ne  3037  pm2.61iine  3038  disjxiun  5163  onfr  6434  f1oprswap  6906  soex  7961  frxp2  8185  frxp3  8192  riiner  8848  difsnen  9119  mapdom2  9214  nnunifi  9355  fofinf1o  9400  brwdom2  9642  cantnff  9743  cantnfp1  9750  carddomi2  10039  wdomfil  10130  fin1a2lem10  10478  fin1a2lem11  10479  uzsupss  13005  xaddcom  13302  xnegdi  13310  xpncan  13313  xleadd1a  13315  xsubge0  13323  ccat1st1st  14676  swrdccatin1  14773  cnpart  15289  fsumcllem  15780  fsumrev2  15830  expcnv  15912  geomulcvg  15924  fprodcllem  15999  fsumdvds  16356  gcd0id  16565  nn0seqcvgd  16617  lcmdvds  16655  mulgcddvds  16702  pcge0  16909  pcneg  16921  pcdvdstr  16923  pcz  16928  pcprmpw2  16929  pcadd  16936  ramcl2  17063  0ramcl  17070  ramub1lem1  17073  ramcl  17076  mrerintcl  17655  mreriincl  17656  mreexexlem4d  17705  mreclatBAD  18633  psgnunilem1  19535  odmulg  19598  sylow1lem1  19640  pgpfi  19647  odadd1  19890  odadd2  19891  gsumval3  19949  gsumpt  20004  dprdfcntz  20059  dprd2da  20086  ablfac1eulem  20116  pgpfaclem3  20127  ablsimpgfind  20154  abvneg  20849  lssssr  20975  lspsneq  21147  lspdisj2  21152  drngnidl  21276  cnsubrg  21468  riinopn  22935  riincld  23073  neipeltop  23158  hauscmplem  23435  cmpfi  23437  ptbasfi  23610  xkoccn  23648  txindislem  23662  txtube  23669  hmphindis  23826  fclscmp  24059  utop2nei  24280  nrginvrcn  24734  nmoleub  24773  blcvx  24839  xrsxmet  24850  xrsblre  24852  lebnumlem3  25014  cphsqrtcl2  25239  ovollb2  25543  ioorcl  25631  i1fmulc  25758  itg1mulc  25759  mbfi1fseqlem4  25773  bddiblnc  25897  dvlip  26052  dvne0  26070  ig1pdvds  26239  plyeq0lem  26269  plyeq0  26270  aannenlem2  26389  aalioulem6  26397  abelthlem8  26501  abelth  26503  cxpexp  26728  cxpge0  26743  cxpmul2  26749  abscxp2  26753  abscxpbnd  26814  cxpeq  26818  nnlogbexp  26842  isosctrlem2  26880  atanrecl  26972  wilthlem2  27130  dchrabs2  27324  dchr1re  27325  lgsneg1  27384  lgsdirprm  27393  lgsdir  27394  lgsne0  27397  lgsdirnn0  27406  lgsdinn0  27407  2sqlem9  27489  rpvmasumlem  27549  dchrvmasumiflem1  27563  dchrisum0flblem1  27570  rpvmasum2  27574  pntrsumbnd2  27629  pntleml  27673  tgcgrextend  28511  tgbtwnexch2  28522  tgifscgr  28534  tgcolg  28580  tgidinside  28597  tgbtwnconn1lem2  28599  tgbtwnconn1lem3  28600  lnhl  28641  tglinethru  28662  tglnpt2  28667  tglineneq  28670  coltr  28673  coltr3  28674  colline  28675  mirreu3  28680  miriso  28696  mirln  28702  mirln2  28703  mirconn  28704  mirbtwnhl  28706  colmid  28714  krippenlem  28716  midexlem  28718  ragflat  28730  ragcgr  28733  perprag  28752  perpdragALT  28753  colperpexlem1  28756  colperpexlem3  28758  midex  28763  opphllem1  28773  opphllem2  28774  opphllem5  28777  opphllem6  28778  hlpasch  28782  lmiisolem  28822  hypcgrlem1  28825  hypcgrlem2  28826  cgrg3col4  28879  upgrex  29127  crctcshwlk  29855  crctcsh  29857  1wlkdlem2  30170  eupth2lem3lem3  30262  eupth2lem3lem7  30266  nmcoplbi  32060  nmophmi  32063  nmbdfnlbi  32081  disjdifprg  32597  imadifxp  32623  2ndimaxp  32665  mptiffisupp  32705  xlt2addrd  32765  ssnnssfz  32792  chnub  32984  gsumpart  33038  symgcntz  33078  fzo0pmtrlast  33085  pmtridf1o  33087  pmtridfv1  33088  pmtridfv2  33089  psgnfzto1stlem  33093  tocycf  33110  cycpmco2lem5  33123  cycpmco2  33126  linds2eq  33374  dvdsruasso  33378  ply1degltel  33580  ply1degleel  33581  ig1pmindeg  33587  fldext2chn  33719  locfinref  33787  zarcmplem  33827  esumpr2  34031  unelldsys  34122  sigapildsyslem  34125  sigapildsys  34126  mbfmcst  34224  carsgsigalem  34280  carsgclctunlem3  34285  pmeasmono  34289  probun  34384  0rrv  34416  sgncl  34503  signsvtn0  34547  signstfvneq0  34549  fineqvac  35073  wevgblacfn  35076  btwnconn1lem11  36061  finxp00  37368  matunitlindf  37578  poimirlem14  37594  mblfinlem1  37617  mblfinlem2  37618  ismblfin  37621  itg2addnclem  37631  itgaddnclem2  37639  areacirclem4  37671  areacirc  37673  isbnd3  37744  blbnd  37747  rrnequiv  37795  lsmsat  38964  lkrscss  39054  eqlkr  39055  lkrshpor  39063  atcvrj2b  39389  atltcvr  39392  3dim1  39424  3dim2  39425  3dim3  39426  ps-2  39435  2at0mat0  39482  dalemdnee  39623  dalem63  39692  lnatexN  39736  2llnma3r  39745  pmodlem1  39803  pmapjat1  39810  pclfinclN  39907  osumclN  39924  pexmidALTN  39935  lhpexle2lem  39966  lhpexle3lem  39968  4atexlemex6  40031  4atex  40033  trlnle  40143  trlval3  40144  cdlemc  40154  cdlemd9  40163  cdleme27N  40326  cdleme28c  40329  cdleme32fvaw  40396  cdleme42ke  40442  cdleme42keg  40443  cdleme42mgN  40445  cdleme17d  40455  cdleme48fvg  40457  cdleme50trn123  40511  cdlemb3  40563  cdlemg8  40588  cdlemg15a  40612  cdlemg15  40613  cdlemg16  40614  cdlemg16ALTN  40615  cdlemg16z  40616  cdlemg16zz  40617  cdlemg20  40642  cdlemg22  40644  cdlemg37  40646  cdlemg31d  40657  cdlemg39  40673  cdlemg40  40674  ltrncom  40695  tendotr  40787  cdlemk25-3  40861  cdlemk35s-id  40895  cdlemk39s-id  40897  cdlemk53b  40913  cdlemk53  40914  cdlemk55  40918  cdlemk35u  40921  cdlemk55u  40923  cdlemk39u  40925  cdlemk19u  40927  cdleml5N  40937  dia2dimlem7  41027  dia2dimlem13  41033  dih1dimatlem  41286  dihlsprn  41288  dihjat1lem  41385  dihjat1  41386  dvh2dim  41402  dochexmid  41425  lclkrlem1  41463  lclkrlem2i  41472  lclkrlem2t  41483  lcfrlem34  41533  lcfrlem38  41537  lcfrlem41  41540  mapdindp1  41677  mapdindp2  41678  mapdh6dN  41696  mapdh6jN  41702  mapdh8j  41744  mapdh8  41745  hdmap1l6d  41770  hdmap1l6j  41776  hdmap11lem2  41799  hdmap14lem7  41831  primrootlekpowne0  42062  aks6d1c7lem2  42138  unitscyglem4  42155  jm2.19  42950  jm2.23  42953  nzss  44286  disjxp1  44971  cnrefiisplem  45750  xlimliminflimsup  45783  stoweidlem58  45979  fourierdlem41  46069  fourierdlem48  46075  fouriersw  46152  etransclem24  46179  nnfoctbdjlem  46376  smfpimltxr  46668  smfpimgtxr  46701  ssnn0ssfz  48074  mreclat  48669