Theorem pm2.61dan 824

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

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

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 210  df-an 401

This theorem is referenced by:  pm2.61ddan  825  pm2.61dda  826  nfsb4t  2531  sbal2  2561  pm2.61danel  3078  ifeq1da  4520  ifeq2da  4521  ifeq12da  4522  ifclda  4524  ifeqda  4525  ifbothda  4527  2if2  4544  somin1  6135  xpcan  6176  fvmpti  6990  fvmptss  7004  funressn  7158  ovima0  7591  ordsuci  7808  suppssov1  8194  suppssov2  8195  oeoa  8584  oeoe  8586  omabs  8638  eceqoveq  8821  domdifsn  9049  pw2f1olem  9070  mapdom1  9131  marypha1lem  9394  supval2  9416  infdifsn  9627  ttrcltr  9686  ttrclselem1  9695  carden2b  9954  fidomtri  9980  dfac12lem2  10129  infunsdom1  10196  infunsdom  10197  itunisuc  10404  gchdomtri  10615  fiminre2  12164  xrmax2  13203  xrmin1  13204  ifle  13224  xnn0lem1lt  13271  xmulneg1  13296  xrsupsslem  13334  xrinfmsslem  13335  fzneuz  13638  seqf1olem1  14079  bccmpl  14347  bcval5  14356  bcpasc  14359  bccl  14360  hasheni  14386  hashfn  14413  hashdom  14417  hashdomi  14418  hashge1  14427  hashbc  14492  pfxval0  14716  sumz  15775  sumss  15777  fsumsplitsn  15797  sumsplit  15821  prod1  16000  prodss  16003  fprodsplitsn  16045  fprodle  16052  bitsmod  16495  sadadd2lem2  16509  sadcaddlem  16516  gcddvds  16562  gcdcl  16565  gcdneg  16581  dvdslcm  16657  lcmcl  16660  lcmneg  16662  lcmgcd  16666  lcmfcl  16687  dvdslcmf  16690  pcgcd  16939  pcmpt  16953  pcmpt2  16954  pcprod  16956  fldivp1  16958  prmreclem4  16980  vdwlem6  17047  ramub1lem1  17087  cidpropd  17767  rescabs  17891  lubval  18411  glbval  18424  joinval  18432  meetval  18446  acsexdimd  18616  gsumpropd2lem  18738  gsumval2  18745  mulgfval  19136  f1otrspeq  19518  pmtrfinv  19532  psgnunilem1  19564  gsumval3  19978  ablfac1c  20144  ablfac1eu  20146  mgpress  20227  orngsqr  20950  frlmsslsp  21927  psrbas  22065  resspsrbas  22104  mplmonmul  22168  mplcoe1  22169  mplcoe5  22172  opsrle  22179  opsrbaslem  22181  psrbaspropd  22375  mplbaspropd  22377  mdetdiag  22737  mdetunilem7  22756  mdetunilem9  22758  maducoeval2  22778  madurid  22782  opnnei  23258  restbas  23296  hauspwdom  23639  ptcmplem5  24194  xrsmopn  24951  xrhmeo  25086  lebnum  25104  pcoass  25164  pcorevlem  25166  icombl  25704  ioombl  25705  mbfconstlem  25767  mbfima  25770  i1fd  25821  mbfi1fseqlem5  25859  itg2const2  25881  itg2seq  25882  itg2uba  25883  itg2splitlem  25888  itg2split  25889  itg2monolem1  25890  itg2gt0  25900  itg2cnlem1  25901  itg2cnlem2  25902  iblss  25945  iblss2  25946  itgss  25952  bddmulibl  25979  coemullem  26388  plymulidp  26424  aaliou2b  26485  isppw2  27260  mule1  27293  ppip1le  27306  dchrelbas3  27383  dchrpt  27412  bposlem3  27431  bposlem5  27433  bposlem6  27434  lgslem4  27445  lgsneg  27466  lgsmod  27468  lgsdilem  27469  lgsdir  27477  lgsdi  27479  lgsne0  27480  lgsquad3  27532  dchrvmasum2if  27642  maxs2  27915  mins1  27916  z12bday  28659  tglnpt4  28909  midexlem  28950  colperpex  28995  outpasch  29018  hlpasch  29019  lnopp2hpgb  29026  lmieu  29074  perpeq  29132  inaghl  29143  cgrg3col4  29151  perpprlng  29181  prlngex  29182  prlngmo2  29187  pthdlem1  30096  nmcfnlbi  32385  elpreq  32855  prssad  32856  prssbd  32857  disjdifprg  32901  disjun0  32921  argcj  33074  f1ocnt  33126  xrge0npcan  33321  psgnfzto1stlem  33401  cyc3genpmlem  33452  cyc3conja  33458  archiabl  33499  erlval  33559  1arithufdlem3  33817  1arithufd  33819  psrmonmul  33921  esplyfval3  33943  resssra  33958  lbslelsp  33969  constrrecl  34140  constrinvcl  34144  constrsqrtcl  34150  1smat1  34175  esumcst  34434  esumrnmpt2  34439  hasheuni  34456  esumcvg  34457  ddemeas  34607  omssubadd  34671  eulerpartlemgc  34733  eulerpartlemb  34739  signswmnd  34925  fineqvnttrclselem1  35515  pthhashvtx  35601  erdsze2lem1  35676  mrsubvrs  35995  unblimceq0lem  37076  unbdqndv2lem2  37080  knoppndvlem10  37091  wl-spae  38157  wl-cbvalnaed  38168  wl-nfeqfb  38172  unccur  38235  poimirlem15  38267  poimirlem22  38274  itg2addnclem  38303  itg2addnclem2  38304  iblmulc2nc  38317  ftc1anclem5  38329  ftc1anc  38333  dvasin  38336  areacirclem5  38344  exmid2  38729  3dim1  40222  3dim2  40223  3dim3  40224  3atlem3  40240  3atlem7  40244  lvolnle3at  40337  2lplnja  40374  paddasslem18  40592  lhpexle3lem  40766  4atex  40831  cdlemd5  40957  cdleme16  41040  cdleme20  41079  cdleme21j  41091  cdleme21  41092  cdleme32snaw  41190  cdleme32fvcl  41195  cdleme32le  41202  cdlemeg46gf  41288  cdleme48gfv  41292  cdleme50trn12  41307  cdlemg6  41378  cdlemg7N  41381  cdlemg38  41470  cdlemg46  41490  dibvalrel  41918  dihlss  42005  dihglblem5aN  42047  dihmeetbN  42058  dihmeetALTN  42082  dihatlat  42089  dihatexv  42093  dvh3dim2  42203  dvh3dim3N  42204  lclkrlem2h  42269  mapdh8d  42538  mapdh8g  42540  hdmap11lem2  42597  lcmineqlem23  42799  aks4d1p3  42826  aks4d1p5  42828  aks4d1p7d1  42830  posbezout  42848  aks6d1c2p2  42867  aks6d1c4  42872  aks6d1c5lem1  42884  aks6d1c6lem3  42920  aks6d1c6lem4  42921  bcled  42926  bcle2d  42927  aks6d1c7  42932  grpods  42942  unitscyglem2  42944  unitscyglem4  42946  aks5lem8  42949  dffltz  43349  ttac  43746  pw2f1ocnv  43747  aomclem5  43768  isnumbasgrplem3  43815  iocmbl  43923  oe0suclim  43987  tfsconcatfv  44051  safesnsupfidom1o  44126  safesnsupfilb  44127  r1rankcld  44938  grur1cld  44939  grucollcld  44953  mnuprd  44969  radcnvrat  45007  bccbc  45038  binomcxp  45050  fnchoice  45732  fiiuncl  45768  eliin2f  45805  founiiun0  45891  axccdom  45921  axccd2  45928  fzisoeu  46002  fperiodmul  46006  upbdrech2  46010  fzdifsuc2  46012  uzfissfz  46025  supxrgere  46032  supxrgelem  46036  supxrge  46037  suplesup  46038  infrpge  46050  xrlexaddrp  46051  xralrple2  46053  infxr  46065  infleinflem1  46068  infleinflem2  46069  infleinf  46070  xralrple3  46072  xrralrecnnge  46088  uzublem  46127  supxrmnf2  46130  infxrpnf  46143  infxrpnf2  46160  supminfxr  46161  supminfxr2  46166  pimxrneun  46185  rexanuz2nf  46189  ioondisj2  46192  iccdifprioo  46215  fmul01lt1lem1  46283  fmul01lt1lem2  46284  limciccioolb  46320  lptioo2  46330  lptioo1  46331  limcicciooub  46334  lptre2pt  46337  limcresiooub  46339  limcresioolb  46340  limcleqr  46341  climfveq  46366  climfveqf  46377  limsupubuzlem  46409  limsupubuz  46410  limsupmnfuzlem  46423  limsupre3uzlem  46432  climxrre  46447  limsup10exlem  46469  cnrefiisplem  46526  climxlim2lem  46542  dfxlim2v  46544  xlimliminflimsup  46559  coskpi2  46563  cosknegpi  46566  icccncfext  46584  cncfiooicclem1  46590  cncfiooicc  46591  cncfiooiccre  46592  dvbdfbdioolem2  46626  ioodvbdlimc1lem1  46628  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  dvnxpaek  46639  dvnprodlem1  46643  dvnprodlem3  46645  volioc  46669  itgioocnicc  46674  iblcncfioo  46675  volico  46680  sublevolico  46681  ismbl3  46683  ovolsplit  46685  volioore  46687  voliooico  46689  voliccico  46696  stoweidlem14  46711  stoweidlem26  46723  stoweidlem28  46725  stoweidlem55  46752  stoweid  46760  stirlinglem5  46775  stirlinglem12  46782  dirkerper  46793  dirkertrigeqlem3  46797  dirkertrigeq  46798  dirkercncflem1  46800  dirkercncflem2  46801  dirkercncf  46804  fourierdlem10  46814  fourierdlem12  46816  fourierdlem24  46828  fourierdlem30  46834  fourierdlem31  46835  fourierdlem32  46836  fourierdlem33  46837  fourierdlem34  46838  fourierdlem35  46839  fourierdlem37  46841  fourierdlem40  46844  fourierdlem41  46845  fourierdlem42  46846  fourierdlem43  46847  fourierdlem44  46848  fourierdlem46  46849  fourierdlem48  46851  fourierdlem49  46852  fourierdlem51  46854  fourierdlem54  46857  fourierdlem62  46865  fourierdlem64  46867  fourierdlem65  46868  fourierdlem70  46873  fourierdlem71  46874  fourierdlem73  46876  fourierdlem74  46877  fourierdlem75  46878  fourierdlem78  46881  fourierdlem79  46882  fourierdlem80  46883  fourierdlem81  46884  fourierdlem82  46885  fourierdlem92  46895  fourierdlem93  46896  fourierdlem97  46900  fourierdlem101  46904  fourierdlem102  46905  fourierdlem103  46906  fourierdlem104  46907  fourierdlem109  46912  fourierdlem114  46917  sqwvfoura  46925  sqwvfourb  46926  fourierswlem  46927  fouriersw  46928  elaa2lem  46930  etransclem15  46946  etransclem19  46950  etransclem20  46951  etransclem22  46953  etransclem23  46954  etransclem24  46955  etransclem25  46956  etransclem27  46958  etransclem28  46959  etransclem35  46966  etransclem38  46969  qndenserrnbl  46992  ioorrnopn  47002  ioorrnopnxrlem  47003  ioorrnopnxr  47004  prsal  47015  salexct  47031  issalnnd  47042  sge0sn  47076  sge0tsms  47077  sge0cl  47078  sge0f1o  47079  sge0sup  47088  sge0less  47089  sge0pr  47091  sge0prle  47098  sge0le  47104  sge0split  47106  sge0splitmpt  47108  sge0iunmptlemfi  47110  sge0iunmpt  47115  sge0isum  47124  sge0xaddlem1  47130  sge0xadd  47132  sge0gtfsumgt  47140  nnfoctbdjlem  47152  iundjiun  47157  meadjun  47159  ismeannd  47164  voliunsge0lem  47169  meaiuninc3v  47181  caragenfiiuncl  47212  omeiunltfirp  47216  carageniuncl  47220  caragenunicl  47221  isomenndlem  47227  isomennd  47228  hoicvr  47245  ovnssle  47258  ovn0  47263  ovnsubadd  47269  hsphoidmvle2  47282  hoidmvval0b  47287  hoidmv1lelem1  47288  hoidmv1lelem2  47289  hoidmv1le  47291  hoidmvlelem2  47293  hoidmvlelem3  47294  hoidmvlelem5  47296  hoidmvle  47297  ovnhoilem1  47298  ovnhoi  47300  ovnlecvr2  47307  hspdifhsp  47313  hoidifhspdmvle  47317  hoiqssbl  47322  hspmbllem1  47323  hspmbllem2  47324  hspmbl  47326  hoimbl  47328  volico2  47338  ovolval2lem  47340  ovnsubadd2lem  47342  ovolval4lem1  47346  ovolval4lem2  47347  ovolval5lem1  47349  vonhoire  47369  iunhoiioo  47373  vonioo  47379  vonicc  47382  vonsn  47388  pimrecltpos  47405  incsmflem  47438  smfpimltxr  47444  smfconst  47446  decsmflem  47463  smfpimgtxr  47477  smfrec  47486  smfpimne2  47537  sharhght  47562  rrx2linest  49505  mofsn2  49606  ipolub00  49754  resccat  49835  initopropdlemlem  50000  prcof1  50149