Theorem pm2.61dane 3033

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 413	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
3		pm2.61dane.2	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)
4	3	ex 413	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
5	2, 4	pm2.61dne 3032	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ≠ wne 2944

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 206  df-an 397  df-ne 2945

This theorem is referenced by:  pm2.61da2ne  3034  pm2.61da3ne  3035  pm2.61iine  3036  disjxiun  5072  onfr  6309  f1oprswap  6769  soex  7777  riiner  8588  difsnen  8849  mapdom2  8944  nnunifi  9074  fofinf1o  9103  brwdom2  9341  cantnff  9441  cantnfp1  9448  carddomi2  9737  wdomfil  9826  fin1a2lem10  10174  fin1a2lem11  10175  uzsupss  12689  xaddcom  12983  xnegdi  12991  xpncan  12994  xleadd1a  12996  xsubge0  13004  ccat1st1st  14344  swrdccatin1  14447  cnpart  14960  fsumcllem  15453  fsumrev2  15503  expcnv  15585  geomulcvg  15597  fprodcllem  15670  fsumdvds  16026  gcd0id  16235  nn0seqcvgd  16284  lcmdvds  16322  mulgcddvds  16369  pcge0  16572  pcneg  16584  pcdvdstr  16586  pcz  16591  pcprmpw2  16592  pcadd  16599  ramcl2  16726  0ramcl  16733  ramub1lem1  16736  ramcl  16739  mrerintcl  17315  mreriincl  17316  mreexexlem4d  17365  mreclatBAD  18290  psgnunilem1  19110  odmulg  19172  sylow1lem1  19212  pgpfi  19219  odadd1  19458  odadd2  19459  gsumval3  19517  gsumpt  19572  dprdfcntz  19627  dprd2da  19654  ablfac1eulem  19684  pgpfaclem3  19695  ablsimpgfind  19722  abvneg  20103  lssssr  20224  lspsneq  20393  lspdisj2  20398  drngnidl  20509  cnsubrg  20667  riinopn  22066  riincld  22204  neipeltop  22289  hauscmplem  22566  cmpfi  22568  ptbasfi  22741  xkoccn  22779  txindislem  22793  txtube  22800  hmphindis  22957  fclscmp  23190  utop2nei  23411  nrginvrcn  23865  nmoleub  23904  blcvx  23970  xrsxmet  23981  xrsblre  23983  lebnumlem3  24135  cphsqrtcl2  24359  ovollb2  24662  ioorcl  24750  i1fmulc  24877  itg1mulc  24878  mbfi1fseqlem4  24892  bddiblnc  25015  dvlip  25166  dvne0  25184  ig1pdvds  25350  plyeq0lem  25380  plyeq0  25381  aannenlem2  25498  aalioulem6  25506  abelthlem8  25607  abelth  25609  cxpexp  25832  cxpge0  25847  cxpmul2  25853  abscxp2  25857  abscxpbnd  25915  cxpeq  25919  nnlogbexp  25940  isosctrlem2  25978  atanrecl  26070  wilthlem2  26227  dchrabs2  26419  dchr1re  26420  lgsneg1  26479  lgsdirprm  26488  lgsdir  26489  lgsne0  26492  lgsdirnn0  26501  lgsdinn0  26502  2sqlem9  26584  rpvmasumlem  26644  dchrvmasumiflem1  26658  dchrisum0flblem1  26665  rpvmasum2  26669  pntrsumbnd2  26724  pntleml  26768  tgcgrextend  26855  tgbtwnexch2  26866  tgifscgr  26878  tgcolg  26924  tgidinside  26941  tgbtwnconn1lem2  26943  tgbtwnconn1lem3  26944  lnhl  26985  tglinethru  27006  tglnpt2  27011  tglineneq  27014  coltr  27017  coltr3  27018  colline  27019  mirreu3  27024  miriso  27040  mirln  27046  mirln2  27047  mirconn  27048  mirbtwnhl  27050  colmid  27058  krippenlem  27060  midexlem  27062  ragflat  27074  ragcgr  27077  perprag  27096  perpdragALT  27097  colperpexlem1  27100  colperpexlem3  27102  midex  27107  opphllem1  27117  opphllem2  27118  opphllem5  27121  opphllem6  27122  hlpasch  27126  lmiisolem  27166  hypcgrlem1  27169  hypcgrlem2  27170  cgrg3col4  27223  upgrex  27471  crctcshwlk  28196  crctcsh  28198  1wlkdlem2  28511  eupth2lem3lem3  28603  eupth2lem3lem7  28607  nmcoplbi  30399  nmophmi  30402  nmbdfnlbi  30420  disjdifprg  30923  imadifxp  30949  2ndimaxp  30993  xlt2addrd  31090  ssnnssfz  31117  gsumpart  31324  symgcntz  31363  pmtridf1o  31370  pmtridfv1  31371  pmtridfv2  31372  psgnfzto1stlem  31376  tocycf  31393  cycpmco2lem5  31406  cycpmco2  31409  linds2eq  31584  locfinref  31800  zarcmplem  31840  esumpr2  32044  unelldsys  32135  sigapildsyslem  32138  sigapildsys  32139  mbfmcst  32235  carsgsigalem  32291  carsgclctunlem3  32296  pmeasmono  32300  probun  32395  0rrv  32427  sgncl  32514  signsvtn0  32558  signstfvneq0  32560  fineqvac  33075  frxp2  33800  frxp3  33806  btwnconn1lem11  34408  finxp00  35582  matunitlindf  35784  poimirlem14  35800  mblfinlem1  35823  mblfinlem2  35824  ismblfin  35827  itg2addnclem  35837  itgaddnclem2  35845  areacirclem4  35877  areacirc  35879  isbnd3  35951  blbnd  35954  rrnequiv  36002  lsmsat  37029  lkrscss  37119  eqlkr  37120  lkrshpor  37128  atcvrj2b  37453  atltcvr  37456  3dim1  37488  3dim2  37489  3dim3  37490  ps-2  37499  2at0mat0  37546  dalemdnee  37687  dalem63  37756  lnatexN  37800  2llnma3r  37809  pmodlem1  37867  pmapjat1  37874  pclfinclN  37971  osumclN  37988  pexmidALTN  37999  lhpexle2lem  38030  lhpexle3lem  38032  4atexlemex6  38095  4atex  38097  trlnle  38207  trlval3  38208  cdlemc  38218  cdlemd9  38227  cdleme27N  38390  cdleme28c  38393  cdleme32fvaw  38460  cdleme42ke  38506  cdleme42keg  38507  cdleme42mgN  38509  cdleme17d  38519  cdleme48fvg  38521  cdleme50trn123  38575  cdlemb3  38627  cdlemg8  38652  cdlemg15a  38676  cdlemg15  38677  cdlemg16  38678  cdlemg16ALTN  38679  cdlemg16z  38680  cdlemg16zz  38681  cdlemg20  38706  cdlemg22  38708  cdlemg37  38710  cdlemg31d  38721  cdlemg39  38737  cdlemg40  38738  ltrncom  38759  tendotr  38851  cdlemk25-3  38925  cdlemk35s-id  38959  cdlemk39s-id  38961  cdlemk53b  38977  cdlemk53  38978  cdlemk55  38982  cdlemk35u  38985  cdlemk55u  38987  cdlemk39u  38989  cdlemk19u  38991  cdleml5N  39001  dia2dimlem7  39091  dia2dimlem13  39097  dih1dimatlem  39350  dihlsprn  39352  dihjat1lem  39449  dihjat1  39450  dvh2dim  39466  dochexmid  39489  lclkrlem1  39527  lclkrlem2i  39536  lclkrlem2t  39547  lcfrlem34  39597  lcfrlem38  39601  lcfrlem41  39604  mapdindp1  39741  mapdindp2  39742  mapdh6dN  39760  mapdh6jN  39766  mapdh8j  39808  mapdh8  39809  hdmap1l6d  39834  hdmap1l6j  39840  hdmap11lem2  39863  hdmap14lem7  39895  jm2.19  40822  jm2.23  40825  nzss  41942  disjxp1  42624  cnrefiisplem  43377  xlimliminflimsup  43410  stoweidlem58  43606  fourierdlem41  43696  fourierdlem48  43702  fouriersw  43779  etransclem24  43806  nnfoctbdjlem  44000  smfpimltxr  44292  smfpimgtxr  44325  ssnn0ssfz  45696  mreclat  46294