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 413	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.61dan.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)
4	3	ex 413	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
5	2, 4	pm2.61d 179	1 ⊢ (𝜑 → 𝜒)

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

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

This theorem is referenced by:  pm2.61ddan  812  pm2.61dda  813  nfsb4t  2498  sbal2  2528  pm2.61danel  3060  ifeq1da  4559  ifeq2da  4560  ifeq12da  4561  ifclda  4563  ifeqda  4564  ifbothda  4566  2if2  4583  somin1  6134  xpcan  6175  fvmpti  6997  fvmptss  7010  funressn  7159  ovima0  7588  ordsuci  7798  oeoa  8599  oeoe  8601  omabs  8652  eceqoveq  8818  domdifsn  9056  pw2f1olem  9078  mapdom1  9144  imafi  9177  marypha1lem  9430  supval2  9452  infdifsn  9654  ttrcltr  9713  ttrclselem1  9722  carden2b  9964  fidomtri  9990  dfac12lem2  10141  infunsdom1  10210  infunsdom  10211  itunisuc  10416  gchdomtri  10626  fiminre2  12164  xrmax2  13157  xrmin1  13158  ifle  13178  xnn0lem1lt  13225  xmulneg1  13250  xrsupsslem  13288  xrinfmsslem  13289  fzneuz  13584  seqf1olem1  14009  bccmpl  14271  bcval5  14280  bcpasc  14283  bccl  14284  hasheni  14310  hashfn  14337  hashdom  14341  hashdomi  14342  hashge1  14351  hashbc  14414  pfxval0  14628  sumz  15670  sumss  15672  fsumsplitsn  15692  sumsplit  15716  prod1  15890  prodss  15893  fprodsplitsn  15935  fprodle  15942  bitsmod  16379  sadadd2lem2  16393  sadcaddlem  16400  gcddvds  16446  gcdcl  16449  gcdneg  16465  dvdslcm  16537  lcmcl  16540  lcmneg  16542  lcmgcd  16546  lcmfcl  16567  dvdslcmf  16570  pcgcd  16813  pcmpt  16827  pcmpt2  16828  pcprod  16830  fldivp1  16832  prmreclem4  16854  vdwlem6  16921  ramub1lem1  16961  cidpropd  17656  rescabs  17784  rescabsOLD  17785  lubval  18311  glbval  18324  joinval  18332  meetval  18346  acsexdimd  18514  gsumpropd2lem  18600  gsumval2  18607  mulgfval  18954  f1otrspeq  19317  pmtrfinv  19331  psgnunilem1  19363  gsumval3  19777  ablfac1c  19943  ablfac1eu  19945  mgpress  20004  mgpressOLD  20005  frlmsslsp  21357  psrbas  21503  resspsrbas  21541  mplmonmul  21597  mplcoe1  21598  mplcoe5  21601  opsrle  21608  opsrbaslem  21610  opsrbaslemOLD  21611  psrbaspropd  21764  mplbaspropd  21766  mdetdiag  22108  mdetunilem7  22127  mdetunilem9  22129  maducoeval2  22149  madurid  22153  opnnei  22631  restbas  22669  hauspwdom  23012  ptcmplem5  23567  xrsmopn  24335  xrhmeo  24469  lebnum  24487  pcoass  24547  pcorevlem  24549  icombl  25088  ioombl  25089  mbfconstlem  25151  mbfima  25154  i1fd  25205  mbfi1fseqlem5  25244  itg2const2  25266  itg2seq  25267  itg2uba  25268  itg2splitlem  25273  itg2split  25274  itg2monolem1  25275  itg2gt0  25285  itg2cnlem1  25286  itg2cnlem2  25287  iblss  25329  iblss2  25330  itgss  25336  bddmulibl  25363  coemullem  25771  aaliou2b  25861  isppw2  26626  mule1  26659  ppip1le  26672  dchrelbas3  26748  dchrpt  26777  bposlem3  26796  bposlem5  26798  bposlem6  26799  lgslem4  26810  lgsneg  26831  lgsmod  26833  lgsdilem  26834  lgsdir  26842  lgsdi  26844  lgsne0  26845  lgsquad3  26897  dchrvmasum2if  27007  maxs2  27276  mins1  27277  midexlem  27981  colperpex  28022  outpasch  28044  hlpasch  28045  lnopp2hpgb  28052  lmieu  28073  inaghl  28134  cgrg3col4  28142  pthdlem1  29061  nmcfnlbi  31343  elpreq  31805  disjdifprg  31844  disjun0  31864  f1ocnt  32051  xrge0npcan  32233  psgnfzto1stlem  32300  cyc3genpmlem  32351  cyc3conja  32357  archiabl  32385  orngsqr  32463  resssra  32733  1smat1  32853  esumcst  33130  esumrnmpt2  33135  hasheuni  33152  esumcvg  33153  ddemeas  33303  omssubadd  33368  eulerpartlemgc  33430  eulerpartlemb  33436  plymulx  33628  signswmnd  33637  pthhashvtx  34187  erdsze2lem1  34263  mrsubvrs  34582  unblimceq0lem  35468  unbdqndv2lem2  35472  knoppndvlem10  35483  wl-spae  36476  wl-cbvalnaed  36487  wl-nfeqfb  36491  unccur  36557  poimirlem15  36589  poimirlem22  36596  itg2addnclem  36625  itg2addnclem2  36626  iblmulc2nc  36639  ftc1anclem5  36651  ftc1anc  36655  dvasin  36658  areacirclem5  36666  exmid2  37053  3dim1  38424  3dim2  38425  3dim3  38426  3atlem3  38442  3atlem7  38446  lvolnle3at  38539  2lplnja  38576  paddasslem18  38794  lhpexle3lem  38968  4atex  39033  cdlemd5  39159  cdleme16  39242  cdleme20  39281  cdleme21j  39293  cdleme21  39294  cdleme32snaw  39392  cdleme32fvcl  39397  cdleme32le  39404  cdlemeg46gf  39490  cdleme48gfv  39494  cdleme50trn12  39509  cdlemg6  39580  cdlemg7N  39583  cdlemg38  39672  cdlemg46  39692  dibvalrel  40120  dihlss  40207  dihglblem5aN  40249  dihmeetbN  40260  dihmeetALTN  40284  dihatlat  40291  dihatexv  40295  dvh3dim2  40405  dvh3dim3N  40406  lclkrlem2h  40471  mapdh8d  40740  mapdh8g  40742  hdmap11lem2  40799  lcmineqlem23  41002  aks4d1p3  41029  aks4d1p5  41031  aks4d1p7d1  41033  aks6d1c2p2  41043  metakunt23  41093  metakunt24  41094  metakunt29  41099  metakunt30  41100  metakunt31  41101  dffltz  41458  ttac  41857  pw2f1ocnv  41858  aomclem5  41882  isnumbasgrplem3  41929  iocmbl  42044  oe0suclim  42109  tfsconcatfv  42173  safesnsupfidom1o  42250  safesnsupfilb  42251  r1rankcld  43072  grur1cld  43073  grucollcld  43101  mnuprd  43117  radcnvrat  43155  bccbc  43186  binomcxp  43198  fnchoice  43795  fiiuncl  43834  eliin2f  43875  founiiun0  43968  axccdom  44000  axccd2  44008  fzisoeu  44089  fperiodmul  44093  upbdrech2  44097  fzdifsuc2  44099  uzfissfz  44115  supxrgere  44122  supxrgelem  44126  supxrge  44127  suplesup  44128  infrpge  44140  xrlexaddrp  44141  xralrple2  44143  infxr  44156  infleinflem1  44159  infleinflem2  44160  infleinf  44161  xralrple3  44163  xrralrecnnge  44179  uzublem  44219  supxrmnf2  44222  infxrpnf  44235  infxrpnf2  44252  supminfxr  44253  supminfxr2  44258  pimxrneun  44278  rexanuz2nf  44282  ioondisj2  44285  iccdifprioo  44308  fmul01lt1lem1  44379  fmul01lt1lem2  44380  limciccioolb  44416  lptioo2  44426  lptioo1  44427  limcicciooub  44432  lptre2pt  44435  limcresiooub  44437  limcresioolb  44438  limcleqr  44439  climfveq  44464  climfveqf  44475  limsupubuzlem  44507  limsupubuz  44508  limsupmnfuzlem  44521  limsupre3uzlem  44530  climxrre  44545  limsup10exlem  44567  cnrefiisplem  44624  climxlim2lem  44640  dfxlim2v  44642  xlimliminflimsup  44657  coskpi2  44661  cosknegpi  44664  icccncfext  44682  cncfiooicclem1  44688  cncfiooicc  44689  cncfiooiccre  44690  dvbdfbdioolem2  44724  ioodvbdlimc1lem1  44726  ioodvbdlimc1lem2  44727  ioodvbdlimc2lem  44729  dvnxpaek  44737  dvnprodlem1  44741  dvnprodlem3  44743  volioc  44767  itgioocnicc  44772  iblcncfioo  44773  volico  44778  sublevolico  44779  ismbl3  44781  ovolsplit  44783  volioore  44785  voliooico  44787  voliccico  44794  stoweidlem14  44809  stoweidlem26  44821  stoweidlem28  44823  stoweidlem55  44850  stoweid  44858  stirlinglem5  44873  stirlinglem12  44880  dirkerper  44891  dirkertrigeqlem3  44895  dirkertrigeq  44896  dirkercncflem1  44898  dirkercncflem2  44899  dirkercncf  44902  fourierdlem10  44912  fourierdlem12  44914  fourierdlem24  44926  fourierdlem30  44932  fourierdlem31  44933  fourierdlem32  44934  fourierdlem33  44935  fourierdlem34  44936  fourierdlem35  44937  fourierdlem37  44939  fourierdlem40  44942  fourierdlem41  44943  fourierdlem42  44944  fourierdlem43  44945  fourierdlem44  44946  fourierdlem46  44947  fourierdlem48  44949  fourierdlem49  44950  fourierdlem51  44952  fourierdlem54  44955  fourierdlem62  44963  fourierdlem64  44965  fourierdlem65  44966  fourierdlem70  44971  fourierdlem71  44972  fourierdlem73  44974  fourierdlem74  44975  fourierdlem75  44976  fourierdlem78  44979  fourierdlem79  44980  fourierdlem80  44981  fourierdlem81  44982  fourierdlem82  44983  fourierdlem92  44993  fourierdlem93  44994  fourierdlem97  44998  fourierdlem101  45002  fourierdlem102  45003  fourierdlem103  45004  fourierdlem104  45005  fourierdlem109  45010  fourierdlem114  45015  sqwvfoura  45023  sqwvfourb  45024  fourierswlem  45025  fouriersw  45026  elaa2lem  45028  etransclem15  45044  etransclem19  45048  etransclem20  45049  etransclem22  45051  etransclem23  45052  etransclem24  45053  etransclem25  45054  etransclem27  45056  etransclem28  45057  etransclem35  45064  etransclem38  45067  qndenserrnbl  45090  ioorrnopn  45100  ioorrnopnxrlem  45101  ioorrnopnxr  45102  prsal  45113  salexct  45129  issalnnd  45140  sge0sn  45174  sge0tsms  45175  sge0cl  45176  sge0f1o  45177  sge0sup  45186  sge0less  45187  sge0pr  45189  sge0prle  45196  sge0le  45202  sge0split  45204  sge0splitmpt  45206  sge0iunmptlemfi  45208  sge0iunmpt  45213  sge0isum  45222  sge0xaddlem1  45228  sge0xadd  45230  sge0gtfsumgt  45238  nnfoctbdjlem  45250  iundjiun  45255  meadjun  45257  ismeannd  45262  voliunsge0lem  45267  meaiuninc3v  45279  caragenfiiuncl  45310  omeiunltfirp  45314  carageniuncl  45318  caragenunicl  45319  isomenndlem  45325  isomennd  45326  hoicvr  45343  ovnssle  45356  ovn0  45361  ovnsubadd  45367  hsphoidmvle2  45380  hoidmvval0b  45385  hoidmv1lelem1  45386  hoidmv1lelem2  45387  hoidmv1le  45389  hoidmvlelem2  45391  hoidmvlelem3  45392  hoidmvlelem5  45394  hoidmvle  45395  ovnhoilem1  45396  ovnhoi  45398  ovnlecvr2  45405  hspdifhsp  45411  hoidifhspdmvle  45415  hoiqssbl  45420  hspmbllem1  45421  hspmbllem2  45422  hspmbl  45424  hoimbl  45426  volico2  45436  ovolval2lem  45438  ovnsubadd2lem  45440  ovolval4lem1  45444  ovolval4lem2  45445  ovolval5lem1  45447  vonhoire  45467  iunhoiioo  45471  vonioo  45477  vonicc  45480  vonsn  45486  pimrecltpos  45503  incsmflem  45536  smfpimltxr  45542  smfconst  45544  decsmflem  45561  smfpimgtxr  45575  smfrec  45584  smfpimne2  45635  sharhght  45660  rrx2linest  47506  mofsn2  47589  ipolub00  47696