Theorem pm2.61dan 825

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm2.61ddan  826  pm2.61dda  827  nfsb4t  2531  sbal2  2561  pm2.61danel  3079  ifeq1da  4517  ifeq2da  4518  ifeq12da  4519  ifclda  4521  ifeqda  4522  ifbothda  4524  2if2  4541  somin1  6143  xpcan  6184  fvmpti  7021  fvmptss  7035  funressn  7193  ovima0  7630  ordsuci  7854  suppssov1  8250  suppssov2  8251  oeoa  8642  oeoe  8644  omabs  8696  eceqoveq  8879  domdifsn  9115  pw2f1olem  9136  mapdom1  9197  marypha1lem  9460  supval2  9482  infdifsn  9693  ttrcltr  9752  ttrclselem1  9761  carden2b  10083  fidomtri  10111  dfac12lem2  10260  infunsdom1  10327  infunsdom  10328  itunisuc  10534  gchdomtri  10751  fiminre2  12303  xrmax2  13344  xrmin1  13345  ifle  13365  xnn0lem1lt  13412  xmulneg1  13437  xrsupsslem  13475  xrinfmsslem  13476  fzneuz  13780  seqf1olem1  14222  bccmpl  14492  bcval5  14501  bcpasc  14504  bccl  14505  hasheni  14531  hashfn  14558  hashdom  14562  hashdomi  14563  hashge1  14572  hashbc  14637  pfxval0  14866  sumz  15929  sumss  15931  fsumsplitsn  15951  sumsplit  15975  prod1  16152  prodss  16155  fprodsplitsn  16197  fprodle  16204  bitsmod  16647  sadadd2lem2  16661  sadcaddlem  16668  gcddvds  16714  gcdcl  16717  gcdneg  16735  dvdslcm  16814  lcmcl  16817  lcmneg  16819  lcmgcd  16823  lcmfcl  16844  dvdslcmf  16847  pcgcd  17097  pcmpt  17111  pcmpt2  17112  pcprod  17114  fldivp1  17116  prmreclem4  17138  vdwlem6  17205  ramub1lem1  17245  cidpropd  17925  rescabs  18049  lubval  18569  glbval  18582  joinval  18590  meetval  18604  acsexdimd  18774  gsumpropd2lem  18909  gsumval2  18916  mulgfval  19320  f1otrspeq  19703  pmtrfinv  19717  psgnunilem1  19749  gsumval3  20163  ablfac1c  20329  ablfac1eu  20331  mgpress  20412  orngsqr  21165  frlmsslsp  22146  psrbas  22286  resspsrbas  22325  mplmonmul  22389  mplcoe1  22390  mplcoe5  22393  opsrle  22400  opsrbaslem  22402  psrbaspropd  22596  mplbaspropd  22598  mdetdiag  22958  mdetunilem7  22977  mdetunilem9  22979  maducoeval2  22999  madurid  23003  opnnei  23482  restbas  23520  hauspwdom  23864  ptcmplem5  24419  xrsmopn  25176  xrhmeo  25311  lebnum  25329  pcoass  25389  pcorevlem  25391  icombl  25929  ioombl  25930  mbfconstlem  25992  mbfima  25995  i1fd  26046  mbfi1fseqlem5  26084  itg2const2  26106  itg2seq  26107  itg2uba  26108  itg2splitlem  26113  itg2split  26114  itg2monolem1  26115  itg2gt0  26125  itg2cnlem1  26126  itg2cnlem2  26127  iblss  26169  iblss2  26170  itgss  26176  bddmulibl  26203  coemullem  26613  plymulidp  26647  aaliou2b  26714  isppw2  27488  mule1  27521  ppip1le  27534  dchrelbas3  27611  dchrpt  27640  bposlem3  27659  bposlem5  27661  bposlem6  27662  lgslem4  27673  lgsneg  27694  lgsmod  27696  lgsdilem  27697  lgsdir  27705  lgsdi  27707  lgsne0  27708  lgsquad3  27760  dchrvmasum2if  27870  maxs2  28173  mins1  28174  z12bday  28917  tglnpt4  29169  midexlem  29210  colperpex  29255  outpasch  29279  hlpasch  29280  lnopp2hpgb  29287  lmieu  29335  perpeq  29394  tgaaddcpbl  29398  inaghl  29410  cgrg3col4  29418  angmgmaddov1lem  29432  angmgmaddrid  29439  perpprlng  29474  prlngex  29475  prlngmo2  29480  pthhashvtx  30361  pthdlem1  30398  nmcfnlbi  32700  elpreq  33212  prssad  33213  prssbd  33214  disjdifprg  33257  disjun0  33277  argcj  33426  f1ocnt  33478  xrge0npcan  33670  psgnfzto1stlem  33750  cyc3genpmlem  33801  cyc3conja  33807  archiabl  33848  erlval  33908  1arithufdlem3  34175  1arithufd  34177  psrmonmul  34286  esplyfval3  34308  resssra  34323  lbslelsp  34334  constrrecl  34505  constrinvcl  34509  constrsqrtcl  34515  1smat1  34540  esumcst  34799  esumrnmpt2  34804  hasheuni  34821  esumcvg  34822  ddemeas  34973  omssubadd  35036  eulerpartlemgc  35098  eulerpartlemb  35104  signswmnd  35290  ecscottd  35878  fineqvnttrclselem1  35923  jltaleph  36060  onf1oracwevd  36086  onprcf1of1ord  36089  erdsze2lem1  36169  mrsubvrs  36488  unblimceq0lem  37580  unbdqndv2lem2  37584  knoppndvlem10  37595  wl-spae  38714  wl-cbvalnaed  38725  wl-nfeqfb  38729  unccur  38787  poimirlem15  38814  poimirlem22  38821  itg2addnclem  38850  itg2addnclem2  38851  iblmulc2nc  38864  ftc1anclem5  38876  ftc1anc  38880  dvasin  38883  areacirclem5  38891  exmid2  39290  3dim1  40783  3dim2  40784  3dim3  40785  3atlem3  40801  3atlem7  40805  lvolnle3at  40898  2lplnja  40935  paddasslem18  41153  lhpexle3lem  41327  4atex  41392  cdlemd5  41518  cdleme16  41601  cdleme20  41640  cdleme21j  41652  cdleme21  41653  cdleme32snaw  41751  cdleme32fvcl  41756  cdleme32le  41763  cdlemeg46gf  41849  cdleme48gfv  41853  cdleme50trn12  41868  cdlemg6  41939  cdlemg7N  41942  cdlemg38  42031  cdlemg46  42051  dibvalrel  42479  dihlss  42566  dihglblem5aN  42608  dihmeetbN  42619  dihmeetALTN  42643  dihatlat  42650  dihatexv  42654  dvh3dim2  42764  dvh3dim3N  42765  lclkrlem2h  42830  mapdh8d  43099  mapdh8g  43101  hdmap11lem2  43158  lcmineqlem23  43360  aks4d1p3  43387  aks4d1p5  43389  aks4d1p7d1  43391  posbezout  43409  aks6d1c2p2  43428  aks6d1c4  43433  aks6d1c5lem1  43445  aks6d1c6lem3  43481  aks6d1c6lem4  43482  bcled  43487  bcle2d  43488  aks6d1c7  43493  grpods  43503  unitscyglem2  43505  unitscyglem4  43507  aks5lem8  43510  dffltz  43930  ttac  44303  pw2f1ocnv  44304  aomclem5  44320  isnumbasgrplem3  44366  iocmbl  44470  oe0suclim  44534  tfsconcatfv  44598  safesnsupfidom1o  44673  safesnsupfilb  44674  r1rankcld  45484  grur1cld  45485  grucollcld  45499  mnuprd  45515  radcnvrat  45553  bccbc  45584  binomcxp  45596  fnchoice  46314  fiiuncl  46350  eliin2f  46386  founiiun0  46472  axccdom  46502  axccd2  46509  fzisoeu  46583  fperiodmul  46587  upbdrech2  46591  fzdifsuc2  46593  uzfissfz  46605  supxrgere  46612  supxrgelem  46616  supxrge  46617  suplesup  46618  infrpge  46630  xrlexaddrp  46631  xralrple2  46633  infxr  46645  infleinflem1  46648  infleinflem2  46649  infleinf  46650  xralrple3  46652  xrralrecnnge  46668  uzublem  46707  supxrmnf2  46710  infxrpnf  46723  infxrpnf2  46740  supminfxr  46741  supminfxr2  46746  pimxrneun  46765  rexanuz2nf  46769  ioondisj2  46772  iccdifprioo  46795  fmul01lt1lem1  46863  fmul01lt1lem2  46864  limciccioolb  46900  lptioo2  46910  lptioo1  46911  limcicciooub  46914  lptre2pt  46917  limcresiooub  46919  limcresioolb  46920  limcleqr  46921  climfveq  46946  climfveqf  46957  limsupubuzlem  46989  limsupubuz  46990  limsupmnfuzlem  47003  limsupre3uzlem  47012  climxrre  47027  limsup10exlem  47049  cnrefiisplem  47106  climxlim2lem  47122  dfxlim2v  47124  xlimliminflimsup  47139  coskpi2  47143  cosknegpi  47146  icccncfext  47164  cncfiooicclem1  47170  cncfiooicc  47171  cncfiooiccre  47172  dvbdfbdioolem2  47206  ioodvbdlimc1lem1  47208  ioodvbdlimc1lem2  47209  ioodvbdlimc2lem  47211  dvnxpaek  47219  dvnprodlem1  47223  dvnprodlem3  47225  volioc  47249  itgioocnicc  47254  iblcncfioo  47255  volico  47260  sublevolico  47261  ismbl3  47263  ovolsplit  47265  volioore  47267  voliooico  47269  voliccico  47276  stoweidlem14  47291  stoweidlem26  47303  stoweidlem28  47305  stoweidlem55  47332  stoweid  47340  stirlinglem5  47355  stirlinglem12  47362  dirkerper  47373  dirkertrigeqlem3  47377  dirkertrigeq  47378  dirkercncflem1  47380  dirkercncflem2  47381  dirkercncf  47384  fourierdlem10  47394  fourierdlem12  47396  fourierdlem24  47408  fourierdlem30  47414  fourierdlem31  47415  fourierdlem32  47416  fourierdlem33  47417  fourierdlem34  47418  fourierdlem35  47419  fourierdlem37  47421  fourierdlem40  47424  fourierdlem41  47425  fourierdlem42  47426  fourierdlem43  47427  fourierdlem44  47428  fourierdlem46  47429  fourierdlem48  47431  fourierdlem49  47432  fourierdlem51  47434  fourierdlem54  47437  fourierdlem62  47445  fourierdlem64  47447  fourierdlem65  47448  fourierdlem70  47453  fourierdlem71  47454  fourierdlem73  47456  fourierdlem74  47457  fourierdlem75  47458  fourierdlem78  47461  fourierdlem79  47462  fourierdlem80  47463  fourierdlem81  47464  fourierdlem82  47465  fourierdlem92  47475  fourierdlem93  47476  fourierdlem97  47480  fourierdlem101  47484  fourierdlem102  47485  fourierdlem103  47486  fourierdlem104  47487  fourierdlem109  47492  fourierdlem114  47497  sqwvfoura  47505  sqwvfourb  47506  fourierswlem  47507  fouriersw  47508  elaa2lem  47510  etransclem15  47526  etransclem19  47530  etransclem20  47531  etransclem22  47533  etransclem23  47534  etransclem24  47535  etransclem25  47536  etransclem27  47538  etransclem28  47539  etransclem35  47546  etransclem38  47549  qndenserrnbl  47572  ioorrnopn  47582  ioorrnopnxrlem  47583  ioorrnopnxr  47584  prsal  47595  salexct  47611  issalnnd  47622  sge0sn  47656  sge0tsms  47657  sge0cl  47658  sge0f1o  47659  sge0sup  47668  sge0less  47669  sge0pr  47671  sge0prle  47678  sge0le  47684  sge0split  47686  sge0splitmpt  47688  sge0iunmptlemfi  47690  sge0iunmpt  47695  sge0isum  47704  sge0xaddlem1  47710  sge0xadd  47712  sge0gtfsumgt  47720  nnfoctbdjlem  47732  iundjiun  47737  meadjun  47739  ismeannd  47744  voliunsge0lem  47749  meaiuninc3v  47761  caragenfiiuncl  47792  omeiunltfirp  47796  carageniuncl  47800  caragenunicl  47801  isomenndlem  47807  isomennd  47808  hoicvr  47825  ovnssle  47838  ovn0  47843  ovnsubadd  47849  hsphoidmvle2  47862  hoidmvval0b  47867  hoidmv1lelem1  47868  hoidmv1lelem2  47869  hoidmv1le  47871  hoidmvlelem2  47873  hoidmvlelem3  47874  hoidmvlelem5  47876  hoidmvle  47877  ovnhoilem1  47878  ovnhoi  47880  ovnlecvr2  47887  hspdifhsp  47893  hoidifhspdmvle  47897  hoiqssbl  47902  hspmbllem1  47903  hspmbllem2  47904  hspmbl  47906  hoimbl  47908  volico2  47918  ovolval2lem  47920  ovnsubadd2lem  47922  ovolval4lem1  47926  ovolval4lem2  47927  ovolval5lem1  47929  vonhoire  47949  iunhoiioo  47953  vonioo  47959  vonicc  47962  vonsn  47968  pimrecltpos  47985  incsmflem  48018  smfpimltxr  48024  smfconst  48026  decsmflem  48043  smfpimgtxr  48057  smfrec  48066  smfpimne2  48117  sharhght  48142  tmachlem-agreeprod  48214  rrx2linest  50179  mofsn2  50281  ipolub00  50432  resccat  50513  initopropdlemlem  50686  prcof1  50848  parcoval2  51091  parmapcl  51096