Theorem pm2.61dan 811

Description: Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)

Hypotheses

Ref	Expression
pm2.61dan.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
pm2.61dan.2	⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)

Assertion

Ref	Expression
pm2.61dan	⊢ (𝜑 → 𝜒)

Proof of Theorem pm2.61dan

Step	Hyp	Ref	Expression
1		pm2.61dan.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 414	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.61dan.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)
4	3	ex 414	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
5	2, 4	pm2.61d 179	1 ⊢ (𝜑 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  pm2.61ddan  812  pm2.61dda  813  nfsb4t  2501  sbal2  2532  pm2.61danel  3061  ifeq1da  4496  ifeq2da  4497  ifeq12da  4498  ifclda  4500  ifeqda  4501  ifbothda  4503  2if2  4520  somin1  6053  xpcan  6094  fvmpti  6906  fvmptss  6919  funressn  7063  ovima0  7483  oeoa  8459  oeoe  8461  omabs  8512  eceqoveq  8642  domdifsn  8879  pw2f1olem  8901  mapdom1  8967  imafi  8996  marypha1lem  9236  supval2  9258  infdifsn  9459  ttrcltr  9518  ttrclselem1  9527  carden2b  9769  fidomtri  9795  dfac12lem2  9946  infunsdom1  10015  infunsdom  10016  itunisuc  10221  gchdomtri  10431  fiminre2  11969  xrmax2  12956  xrmin1  12957  ifle  12977  xnn0lem1lt  13024  xmulneg1  13049  xrsupsslem  13087  xrinfmsslem  13088  fzneuz  13383  seqf1olem1  13808  bccmpl  14069  bcval5  14078  bcpasc  14081  bccl  14082  hasheni  14108  hashfn  14135  hashdom  14139  hashdomi  14140  hashge1  14149  hashbc  14210  pfxval0  14434  sumz  15479  sumss  15481  fsumsplitsn  15501  sumsplit  15525  prod1  15699  prodss  15702  fprodsplitsn  15744  fprodle  15751  bitsmod  16188  sadadd2lem2  16202  sadcaddlem  16209  gcddvds  16255  gcdcl  16258  gcdneg  16274  dvdslcm  16348  lcmcl  16351  lcmneg  16353  lcmgcd  16357  lcmfcl  16378  dvdslcmf  16381  pcgcd  16624  pcmpt  16638  pcmpt2  16639  pcprod  16641  fldivp1  16643  prmreclem4  16665  vdwlem6  16732  ramub1lem1  16772  cidpropd  17464  rescabs  17592  rescabsOLD  17593  lubval  18119  glbval  18132  joinval  18140  meetval  18154  acsexdimd  18322  gsumpropd2lem  18408  gsumval2  18415  mulgfval  18747  f1otrspeq  19100  pmtrfinv  19114  psgnunilem1  19146  gsumval3  19553  ablfac1c  19719  ablfac1eu  19721  mgpress  19780  mgpressOLD  19781  frlmsslsp  21048  psrbas  21192  resspsrbas  21229  mplmonmul  21282  mplcoe1  21283  mplcoe5  21286  opsrle  21293  opsrbaslem  21295  opsrbaslemOLD  21296  psrbaspropd  21451  mplbaspropd  21453  mdetdiag  21793  mdetunilem7  21812  mdetunilem9  21814  maducoeval2  21834  madurid  21838  opnnei  22316  restbas  22354  hauspwdom  22697  ptcmplem5  23252  xrsmopn  24020  xrhmeo  24154  lebnum  24172  pcoass  24232  pcorevlem  24234  icombl  24773  ioombl  24774  mbfconstlem  24836  mbfima  24839  i1fd  24890  mbfi1fseqlem5  24929  itg2const2  24951  itg2seq  24952  itg2uba  24953  itg2splitlem  24958  itg2split  24959  itg2monolem1  24960  itg2gt0  24970  itg2cnlem1  24971  itg2cnlem2  24972  iblss  25014  iblss2  25015  itgss  25021  bddmulibl  25048  coemullem  25456  aaliou2b  25546  isppw2  26309  mule1  26342  ppip1le  26355  dchrelbas3  26431  dchrpt  26460  bposlem3  26479  bposlem5  26481  bposlem6  26482  lgslem4  26493  lgsneg  26514  lgsmod  26516  lgsdilem  26517  lgsdir  26525  lgsdi  26527  lgsne0  26528  lgsquad3  26580  dchrvmasum2if  26690  midexlem  27098  colperpex  27139  outpasch  27161  hlpasch  27162  lnopp2hpgb  27169  lmieu  27190  inaghl  27251  cgrg3col4  27259  pthdlem1  28179  nmcfnlbi  30459  elpreq  30923  disjdifprg  30959  disjun0  30979  f1ocnt  31168  xrge0npcan  31348  psgnfzto1stlem  31412  cyc3genpmlem  31463  cyc3conja  31469  archiabl  31497  orngsqr  31548  1smat1  31799  esumcst  32076  esumrnmpt2  32081  hasheuni  32098  esumcvg  32099  ddemeas  32249  omssubadd  32312  eulerpartlemgc  32374  eulerpartlemb  32380  plymulx  32572  signswmnd  32581  pthhashvtx  33134  erdsze2lem1  33210  mrsubvrs  33529  unblimceq0lem  34731  unbdqndv2lem2  34735  knoppndvlem10  34746  wl-spae  35724  wl-cbvalnaed  35735  wl-nfeqfb  35739  unccur  35804  poimirlem15  35836  poimirlem22  35843  itg2addnclem  35872  itg2addnclem2  35873  iblmulc2nc  35886  ftc1anclem5  35898  ftc1anc  35902  dvasin  35905  areacirclem5  35913  exmid2  36301  3dim1  37523  3dim2  37524  3dim3  37525  3atlem3  37541  3atlem7  37545  lvolnle3at  37638  2lplnja  37675  paddasslem18  37893  lhpexle3lem  38067  4atex  38132  cdlemd5  38258  cdleme16  38341  cdleme20  38380  cdleme21j  38392  cdleme21  38393  cdleme32snaw  38491  cdleme32fvcl  38496  cdleme32le  38503  cdlemeg46gf  38589  cdleme48gfv  38593  cdleme50trn12  38608  cdlemg6  38679  cdlemg7N  38682  cdlemg38  38771  cdlemg46  38791  dibvalrel  39219  dihlss  39306  dihglblem5aN  39348  dihmeetbN  39359  dihmeetALTN  39383  dihatlat  39390  dihatexv  39394  dvh3dim2  39504  dvh3dim3N  39505  lclkrlem2h  39570  mapdh8d  39839  mapdh8g  39841  hdmap11lem2  39898  lcmineqlem23  40101  aks4d1p3  40128  aks4d1p5  40130  aks4d1p7d1  40132  metakunt23  40189  metakunt24  40190  metakunt29  40195  metakunt30  40196  metakunt31  40197  dffltz  40508  ttac  40896  pw2f1ocnv  40897  aomclem5  40921  isnumbasgrplem3  40968  iocmbl  41082  r1rankcld  41887  grur1cld  41888  grucollcld  41916  mnuprd  41932  radcnvrat  41970  bccbc  42001  binomcxp  42013  fnchoice  42610  fiiuncl  42651  eliin2f  42692  founiiun0  42772  axccdom  42806  axccd2  42814  fzisoeu  42887  fperiodmul  42891  upbdrech2  42895  fzdifsuc2  42897  uzfissfz  42913  supxrgere  42920  supxrgelem  42924  supxrge  42925  suplesup  42926  infrpge  42938  xrlexaddrp  42939  xralrple2  42941  infxr  42954  infleinflem1  42957  infleinflem2  42958  infleinf  42959  xralrple3  42961  xrralrecnnge  42978  uzublem  43018  supxrmnf2  43021  infxrpnf  43034  infxrpnf2  43051  supminfxr  43052  supminfxr2  43057  pimxrneun  43077  ioondisj2  43080  iccdifprioo  43103  fmul01lt1lem1  43174  fmul01lt1lem2  43175  limciccioolb  43211  lptioo2  43221  lptioo1  43222  limcicciooub  43227  lptre2pt  43230  limcresiooub  43232  limcresioolb  43233  limcleqr  43234  climfveq  43259  climfveqf  43270  limsupubuzlem  43302  limsupubuz  43303  limsupmnfuzlem  43316  limsupre3uzlem  43325  climxrre  43340  limsup10exlem  43362  cnrefiisplem  43419  climxlim2lem  43435  dfxlim2v  43437  xlimliminflimsup  43452  coskpi2  43456  cosknegpi  43459  icccncfext  43477  cncfiooicclem1  43483  cncfiooicc  43484  cncfiooiccre  43485  dvbdfbdioolem2  43519  ioodvbdlimc1lem1  43521  ioodvbdlimc1lem2  43522  ioodvbdlimc2lem  43524  dvnxpaek  43532  dvnprodlem1  43536  dvnprodlem3  43538  volioc  43562  itgioocnicc  43567  iblcncfioo  43568  volico  43573  sublevolico  43574  ismbl3  43576  ovolsplit  43578  volioore  43580  voliooico  43582  voliccico  43589  stoweidlem14  43604  stoweidlem26  43616  stoweidlem28  43618  stoweidlem55  43645  stoweid  43653  stirlinglem5  43668  stirlinglem12  43675  dirkerper  43686  dirkertrigeqlem3  43690  dirkertrigeq  43691  dirkercncflem1  43693  dirkercncflem2  43694  dirkercncf  43697  fourierdlem10  43707  fourierdlem12  43709  fourierdlem24  43721  fourierdlem30  43727  fourierdlem31  43728  fourierdlem32  43729  fourierdlem33  43730  fourierdlem34  43731  fourierdlem35  43732  fourierdlem37  43734  fourierdlem40  43737  fourierdlem41  43738  fourierdlem42  43739  fourierdlem43  43740  fourierdlem44  43741  fourierdlem46  43742  fourierdlem48  43744  fourierdlem49  43745  fourierdlem51  43747  fourierdlem54  43750  fourierdlem62  43758  fourierdlem64  43760  fourierdlem65  43761  fourierdlem70  43766  fourierdlem71  43767  fourierdlem73  43769  fourierdlem74  43770  fourierdlem75  43771  fourierdlem78  43774  fourierdlem79  43775  fourierdlem80  43776  fourierdlem81  43777  fourierdlem82  43778  fourierdlem92  43788  fourierdlem93  43789  fourierdlem97  43793  fourierdlem101  43797  fourierdlem102  43798  fourierdlem103  43799  fourierdlem104  43800  fourierdlem109  43805  fourierdlem114  43810  sqwvfoura  43818  sqwvfourb  43819  fourierswlem  43820  fouriersw  43821  elaa2lem  43823  etransclem15  43839  etransclem19  43843  etransclem20  43844  etransclem22  43846  etransclem23  43847  etransclem24  43848  etransclem25  43849  etransclem27  43851  etransclem28  43852  etransclem35  43859  etransclem38  43862  qndenserrnbl  43885  ioorrnopn  43895  ioorrnopnxrlem  43896  ioorrnopnxr  43897  prsal  43908  salexct  43922  issalnnd  43933  sge0sn  43967  sge0tsms  43968  sge0cl  43969  sge0f1o  43970  sge0sup  43979  sge0less  43980  sge0pr  43982  sge0prle  43989  sge0le  43995  sge0split  43997  sge0splitmpt  43999  sge0iunmptlemfi  44001  sge0iunmpt  44006  sge0isum  44015  sge0xaddlem1  44021  sge0xadd  44023  sge0gtfsumgt  44031  nnfoctbdjlem  44043  iundjiun  44048  meadjun  44050  ismeannd  44055  voliunsge0lem  44060  meaiuninc3v  44072  caragenfiiuncl  44103  omeiunltfirp  44107  carageniuncl  44111  caragenunicl  44112  isomenndlem  44118  isomennd  44119  hoicvr  44136  ovnssle  44149  ovn0  44154  ovnsubadd  44160  hsphoidmvle2  44173  hoidmvval0b  44178  hoidmv1lelem1  44179  hoidmv1lelem2  44180  hoidmv1le  44182  hoidmvlelem2  44184  hoidmvlelem3  44185  hoidmvlelem5  44187  hoidmvle  44188  ovnhoilem1  44189  ovnhoi  44191  ovnlecvr2  44198  hspdifhsp  44204  hoidifhspdmvle  44208  hoiqssbl  44213  hspmbllem1  44214  hspmbllem2  44215  hspmbl  44217  hoimbl  44219  volico2  44229  ovolval2lem  44231  ovnsubadd2lem  44233  ovolval4lem1  44237  ovolval4lem2  44238  ovolval5lem1  44240  vonhoire  44260  iunhoiioo  44264  vonioo  44270  vonicc  44273  vonsn  44279  pimrecltpos  44296  incsmflem  44329  smfpimltxr  44335  smfconst  44337  decsmflem  44354  smfpimgtxr  44368  smfrec  44377  sharhght  44439  rrx2linest  46146  mofsn2  46230  ipolub00  46337