Theorem pm2.61dan 813

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

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

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

This theorem is referenced by:  pm2.61ddan  814  pm2.61dda  815  nfsb4t  2503  sbal2  2533  pm2.61danel  3050  ifeq1da  4498  ifeq2da  4499  ifeq12da  4500  ifclda  4502  ifeqda  4503  ifbothda  4505  2if2  4522  somin1  6096  xpcan  6140  fvmpti  6946  fvmptss  6960  funressn  7113  ovima0  7546  ordsuci  7762  suppssov1  8147  suppssov2  8148  oeoa  8533  oeoe  8535  omabs  8587  eceqoveq  8769  domdifsn  8998  pw2f1olem  9019  mapdom1  9080  imafiOLD  9226  marypha1lem  9346  supval2  9368  infdifsn  9578  ttrcltr  9637  ttrclselem1  9646  carden2b  9891  fidomtri  9917  dfac12lem2  10067  infunsdom1  10134  infunsdom  10135  itunisuc  10341  gchdomtri  10552  fiminre2  12104  xrmax2  13128  xrmin1  13129  ifle  13149  xnn0lem1lt  13196  xmulneg1  13221  xrsupsslem  13259  xrinfmsslem  13260  fzneuz  13562  seqf1olem1  14003  bccmpl  14271  bcval5  14280  bcpasc  14283  bccl  14284  hasheni  14310  hashfn  14337  hashdom  14341  hashdomi  14342  hashge1  14351  hashbc  14415  pfxval0  14639  sumz  15684  sumss  15686  fsumsplitsn  15706  sumsplit  15730  prod1  15909  prodss  15912  fprodsplitsn  15954  fprodle  15961  bitsmod  16405  sadadd2lem2  16419  sadcaddlem  16426  gcddvds  16472  gcdcl  16475  gcdneg  16491  dvdslcm  16567  lcmcl  16570  lcmneg  16572  lcmgcd  16576  lcmfcl  16597  dvdslcmf  16600  pcgcd  16849  pcmpt  16863  pcmpt2  16864  pcprod  16866  fldivp1  16868  prmreclem4  16890  vdwlem6  16957  ramub1lem1  16997  cidpropd  17676  rescabs  17800  lubval  18320  glbval  18333  joinval  18341  meetval  18355  acsexdimd  18525  gsumpropd2lem  18647  gsumval2  18654  mulgfval  19045  f1otrspeq  19422  pmtrfinv  19436  psgnunilem1  19468  gsumval3  19882  ablfac1c  20048  ablfac1eu  20050  mgpress  20131  orngsqr  20843  frlmsslsp  21776  psrbas  21913  resspsrbas  21952  mplmonmul  22014  mplcoe1  22015  mplcoe5  22018  opsrle  22025  opsrbaslem  22027  psrbaspropd  22198  mplbaspropd  22200  mdetdiag  22564  mdetunilem7  22583  mdetunilem9  22585  maducoeval2  22605  madurid  22609  opnnei  23085  restbas  23123  hauspwdom  23466  ptcmplem5  24021  xrsmopn  24778  xrhmeo  24913  lebnum  24931  pcoass  24991  pcorevlem  24993  icombl  25531  ioombl  25532  mbfconstlem  25594  mbfima  25597  i1fd  25648  mbfi1fseqlem5  25686  itg2const2  25708  itg2seq  25709  itg2uba  25710  itg2splitlem  25715  itg2split  25716  itg2monolem1  25717  itg2gt0  25727  itg2cnlem1  25728  itg2cnlem2  25729  iblss  25772  iblss2  25773  itgss  25779  bddmulibl  25806  coemullem  26215  aaliou2b  26307  isppw2  27078  mule1  27111  ppip1le  27124  dchrelbas3  27201  dchrpt  27230  bposlem3  27249  bposlem5  27251  bposlem6  27252  lgslem4  27263  lgsneg  27284  lgsmod  27286  lgsdilem  27287  lgsdir  27295  lgsdi  27297  lgsne0  27298  lgsquad3  27350  dchrvmasum2if  27460  maxs2  27734  mins1  27735  z12bday  28477  midexlem  28760  colperpex  28801  outpasch  28823  hlpasch  28824  lnopp2hpgb  28831  lmieu  28852  inaghl  28913  cgrg3col4  28921  pthdlem1  29834  nmcfnlbi  32123  elpreq  32598  prssad  32599  prssbd  32600  disjdifprg  32645  disjun0  32665  argcj  32821  f1ocnt  32873  xrge0npcan  33080  psgnfzto1stlem  33161  cyc3genpmlem  33212  cyc3conja  33218  archiabl  33259  erlval  33319  1arithufdlem3  33606  1arithufd  33608  psrmonmul  33694  esplyfval3  33716  resssra  33731  lbslelsp  33742  constrrecl  33913  constrinvcl  33917  constrsqrtcl  33923  1smat1  33948  esumcst  34207  esumrnmpt2  34212  hasheuni  34229  esumcvg  34230  ddemeas  34380  omssubadd  34444  eulerpartlemgc  34506  eulerpartlemb  34512  plymulx  34692  signswmnd  34701  fineqvnttrclselem1  35265  pthhashvtx  35310  erdsze2lem1  35385  mrsubvrs  35704  unblimceq0lem  36766  unbdqndv2lem2  36770  knoppndvlem10  36781  wl-spae  37846  wl-cbvalnaed  37857  wl-nfeqfb  37861  unccur  37924  poimirlem15  37956  poimirlem22  37963  itg2addnclem  37992  itg2addnclem2  37993  iblmulc2nc  38006  ftc1anclem5  38018  ftc1anc  38022  dvasin  38025  areacirclem5  38033  exmid2  38420  3dim1  39913  3dim2  39914  3dim3  39915  3atlem3  39931  3atlem7  39935  lvolnle3at  40028  2lplnja  40065  paddasslem18  40283  lhpexle3lem  40457  4atex  40522  cdlemd5  40648  cdleme16  40731  cdleme20  40770  cdleme21j  40782  cdleme21  40783  cdleme32snaw  40881  cdleme32fvcl  40886  cdleme32le  40893  cdlemeg46gf  40979  cdleme48gfv  40983  cdleme50trn12  40998  cdlemg6  41069  cdlemg7N  41072  cdlemg38  41161  cdlemg46  41181  dibvalrel  41609  dihlss  41696  dihglblem5aN  41738  dihmeetbN  41749  dihmeetALTN  41773  dihatlat  41780  dihatexv  41784  dvh3dim2  41894  dvh3dim3N  41895  lclkrlem2h  41960  mapdh8d  42229  mapdh8g  42231  hdmap11lem2  42288  lcmineqlem23  42490  aks4d1p3  42517  aks4d1p5  42519  aks4d1p7d1  42521  posbezout  42539  aks6d1c2p2  42558  aks6d1c4  42563  aks6d1c5lem1  42575  aks6d1c6lem3  42611  aks6d1c6lem4  42612  bcled  42617  bcle2d  42618  aks6d1c7  42623  grpods  42633  unitscyglem2  42635  unitscyglem4  42637  aks5lem8  42640  dffltz  43067  ttac  43464  pw2f1ocnv  43465  aomclem5  43486  isnumbasgrplem3  43533  iocmbl  43641  oe0suclim  43705  tfsconcatfv  43769  safesnsupfidom1o  43844  safesnsupfilb  43845  r1rankcld  44658  grur1cld  44659  grucollcld  44687  mnuprd  44703  radcnvrat  44741  bccbc  44772  binomcxp  44784  fnchoice  45460  fiiuncl  45496  eliin2f  45534  founiiun0  45620  axccdom  45651  axccd2  45659  fzisoeu  45733  fperiodmul  45737  upbdrech2  45741  fzdifsuc2  45743  uzfissfz  45756  supxrgere  45763  supxrgelem  45767  supxrge  45768  suplesup  45769  infrpge  45781  xrlexaddrp  45782  xralrple2  45784  infxr  45796  infleinflem1  45799  infleinflem2  45800  infleinf  45801  xralrple3  45803  xrralrecnnge  45819  uzublem  45858  supxrmnf2  45861  infxrpnf  45874  infxrpnf2  45891  supminfxr  45892  supminfxr2  45897  pimxrneun  45916  rexanuz2nf  45920  ioondisj2  45923  iccdifprioo  45946  fmul01lt1lem1  46014  fmul01lt1lem2  46015  limciccioolb  46051  lptioo2  46061  lptioo1  46062  limcicciooub  46065  lptre2pt  46068  limcresiooub  46070  limcresioolb  46071  limcleqr  46072  climfveq  46097  climfveqf  46108  limsupubuzlem  46140  limsupubuz  46141  limsupmnfuzlem  46154  limsupre3uzlem  46163  climxrre  46178  limsup10exlem  46200  cnrefiisplem  46257  climxlim2lem  46273  dfxlim2v  46275  xlimliminflimsup  46290  coskpi2  46294  cosknegpi  46297  icccncfext  46315  cncfiooicclem1  46321  cncfiooicc  46322  cncfiooiccre  46323  dvbdfbdioolem2  46357  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnxpaek  46370  dvnprodlem1  46374  dvnprodlem3  46376  volioc  46400  itgioocnicc  46405  iblcncfioo  46406  volico  46411  sublevolico  46412  ismbl3  46414  ovolsplit  46416  volioore  46418  voliooico  46420  voliccico  46427  stoweidlem14  46442  stoweidlem26  46454  stoweidlem28  46456  stoweidlem55  46483  stoweid  46491  stirlinglem5  46506  stirlinglem12  46513  dirkerper  46524  dirkertrigeqlem3  46528  dirkertrigeq  46529  dirkercncflem1  46531  dirkercncflem2  46532  dirkercncf  46535  fourierdlem10  46545  fourierdlem12  46547  fourierdlem24  46559  fourierdlem30  46565  fourierdlem31  46566  fourierdlem32  46567  fourierdlem33  46568  fourierdlem34  46569  fourierdlem35  46570  fourierdlem37  46572  fourierdlem40  46575  fourierdlem41  46576  fourierdlem42  46577  fourierdlem43  46578  fourierdlem44  46579  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem51  46585  fourierdlem54  46588  fourierdlem62  46596  fourierdlem64  46598  fourierdlem65  46599  fourierdlem70  46604  fourierdlem71  46605  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem78  46612  fourierdlem79  46613  fourierdlem80  46614  fourierdlem81  46615  fourierdlem82  46616  fourierdlem92  46626  fourierdlem93  46627  fourierdlem97  46631  fourierdlem101  46635  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem109  46643  fourierdlem114  46648  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  elaa2lem  46661  etransclem15  46677  etransclem19  46681  etransclem20  46682  etransclem22  46684  etransclem23  46685  etransclem24  46686  etransclem25  46687  etransclem27  46689  etransclem28  46690  etransclem35  46697  etransclem38  46700  qndenserrnbl  46723  ioorrnopn  46733  ioorrnopnxrlem  46734  ioorrnopnxr  46735  prsal  46746  salexct  46762  issalnnd  46773  sge0sn  46807  sge0tsms  46808  sge0cl  46809  sge0f1o  46810  sge0sup  46819  sge0less  46820  sge0pr  46822  sge0prle  46829  sge0le  46835  sge0split  46837  sge0splitmpt  46839  sge0iunmptlemfi  46841  sge0iunmpt  46846  sge0isum  46855  sge0xaddlem1  46861  sge0xadd  46863  sge0gtfsumgt  46871  nnfoctbdjlem  46883  iundjiun  46888  meadjun  46890  ismeannd  46895  voliunsge0lem  46900  meaiuninc3v  46912  caragenfiiuncl  46943  omeiunltfirp  46947  carageniuncl  46951  caragenunicl  46952  isomenndlem  46958  isomennd  46959  hoicvr  46976  ovnssle  46989  ovn0  46994  ovnsubadd  47000  hsphoidmvle2  47013  hoidmvval0b  47018  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1le  47022  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem5  47027  hoidmvle  47028  ovnhoilem1  47029  ovnhoi  47031  ovnlecvr2  47038  hspdifhsp  47044  hoidifhspdmvle  47048  hoiqssbl  47053  hspmbllem1  47054  hspmbllem2  47055  hspmbl  47057  hoimbl  47059  volico2  47069  ovolval2lem  47071  ovnsubadd2lem  47073  ovolval4lem1  47077  ovolval4lem2  47078  ovolval5lem1  47080  vonhoire  47100  iunhoiioo  47104  vonioo  47110  vonicc  47113  vonsn  47119  pimrecltpos  47136  incsmflem  47169  smfpimltxr  47175  smfconst  47177  decsmflem  47194  smfpimgtxr  47208  smfrec  47217  smfpimne2  47268  sharhght  47293  rrx2linest  49218  mofsn2  49320  ipolub00  49468  resccat  49549  initopropdlemlem  49714  prcof1  49863