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  2528  sbal2  2558  pm2.61danel  3075  ifeq1da  4513  ifeq2da  4514  ifeq12da  4515  ifclda  4517  ifeqda  4518  ifbothda  4520  2if2  4537  somin1  6126  xpcan  6167  fvmpti  6993  fvmptss  7007  funressn  7164  ovima0  7601  ordsuci  7823  suppssov1  8218  suppssov2  8219  oeoa  8610  oeoe  8612  omabs  8664  eceqoveq  8847  domdifsn  9083  pw2f1olem  9104  mapdom1  9165  marypha1lem  9429  supval2  9451  infdifsn  9662  ttrcltr  9721  ttrclselem1  9730  carden2b  10052  fidomtri  10078  dfac12lem2  10227  infunsdom1  10294  infunsdom  10295  itunisuc  10501  gchdomtri  10718  fiminre2  12269  xrmax2  13310  xrmin1  13311  ifle  13331  xnn0lem1lt  13378  xmulneg1  13403  xrsupsslem  13441  xrinfmsslem  13442  fzneuz  13746  seqf1olem1  14188  bccmpl  14457  bcval5  14466  bcpasc  14469  bccl  14470  hasheni  14496  hashfn  14523  hashdom  14527  hashdomi  14528  hashge1  14537  hashbc  14602  pfxval0  14831  sumz  15894  sumss  15896  fsumsplitsn  15916  sumsplit  15940  prod1  16117  prodss  16120  fprodsplitsn  16162  fprodle  16169  bitsmod  16612  sadadd2lem2  16626  sadcaddlem  16633  gcddvds  16679  gcdcl  16682  gcdneg  16700  dvdslcm  16779  lcmcl  16782  lcmneg  16784  lcmgcd  16788  lcmfcl  16809  dvdslcmf  16812  pcgcd  17062  pcmpt  17076  pcmpt2  17077  pcprod  17079  fldivp1  17081  prmreclem4  17103  vdwlem6  17170  ramub1lem1  17210  cidpropd  17890  rescabs  18014  lubval  18534  glbval  18547  joinval  18555  meetval  18569  acsexdimd  18739  gsumpropd2lem  18874  gsumval2  18881  mulgfval  19285  f1otrspeq  19667  pmtrfinv  19681  psgnunilem1  19713  gsumval3  20127  ablfac1c  20293  ablfac1eu  20295  mgpress  20376  orngsqr  21129  frlmsslsp  22108  psrbas  22248  resspsrbas  22287  mplmonmul  22351  mplcoe1  22352  mplcoe5  22355  opsrle  22362  opsrbaslem  22364  psrbaspropd  22558  mplbaspropd  22560  mdetdiag  22920  mdetunilem7  22939  mdetunilem9  22941  maducoeval2  22961  madurid  22965  opnnei  23444  restbas  23482  hauspwdom  23826  ptcmplem5  24381  xrsmopn  25138  xrhmeo  25273  lebnum  25291  pcoass  25351  pcorevlem  25353  icombl  25891  ioombl  25892  mbfconstlem  25954  mbfima  25957  i1fd  26008  mbfi1fseqlem5  26046  itg2const2  26068  itg2seq  26069  itg2uba  26070  itg2splitlem  26075  itg2split  26076  itg2monolem1  26077  itg2gt0  26087  itg2cnlem1  26088  itg2cnlem2  26089  iblss  26131  iblss2  26132  itgss  26138  bddmulibl  26165  coemullem  26575  plymulidp  26609  aaliou2b  26674  isppw2  27448  mule1  27481  ppip1le  27494  dchrelbas3  27571  dchrpt  27600  bposlem3  27619  bposlem5  27621  bposlem6  27622  lgslem4  27633  lgsneg  27654  lgsmod  27656  lgsdilem  27657  lgsdir  27665  lgsdi  27667  lgsne0  27668  lgsquad3  27720  dchrvmasum2if  27830  maxs2  28133  mins1  28134  z12bday  28877  tglnpt4  29129  midexlem  29170  colperpex  29215  outpasch  29239  hlpasch  29240  lnopp2hpgb  29247  lmieu  29295  perpeq  29354  tgaaddcpbl  29358  inaghl  29370  cgrg3col4  29378  angmgmaddov1lem  29392  angmgmaddrid  29399  perpprlng  29434  prlngex  29435  prlngmo2  29440  pthhashvtx  30321  pthdlem1  30358  nmcfnlbi  32660  elpreq  33172  prssad  33173  prssbd  33174  disjdifprg  33217  disjun0  33237  argcj  33387  f1ocnt  33439  xrge0npcan  33628  psgnfzto1stlem  33708  cyc3genpmlem  33759  cyc3conja  33765  archiabl  33806  erlval  33866  1arithufdlem3  34125  1arithufd  34127  psrmonmul  34229  esplyfval3  34251  resssra  34266  lbslelsp  34277  constrrecl  34448  constrinvcl  34452  constrsqrtcl  34458  1smat1  34483  esumcst  34742  esumrnmpt2  34747  hasheuni  34764  esumcvg  34765  ddemeas  34916  omssubadd  34979  eulerpartlemgc  35041  eulerpartlemb  35047  signswmnd  35233  fineqvnttrclselem1  35846  onf1oracwevd  35972  onprcf1of1ord  35975  erdsze2lem1  36055  mrsubvrs  36374  unblimceq0lem  37465  unbdqndv2lem2  37469  knoppndvlem10  37480  wl-spae  38547  wl-cbvalnaed  38558  wl-nfeqfb  38562  unccur  38620  poimirlem15  38647  poimirlem22  38654  itg2addnclem  38683  itg2addnclem2  38684  iblmulc2nc  38697  ftc1anclem5  38709  ftc1anc  38713  dvasin  38716  areacirclem5  38724  exmid2  39125  3dim1  40618  3dim2  40619  3dim3  40620  3atlem3  40636  3atlem7  40640  lvolnle3at  40733  2lplnja  40770  paddasslem18  40988  lhpexle3lem  41162  4atex  41227  cdlemd5  41353  cdleme16  41436  cdleme20  41475  cdleme21j  41487  cdleme21  41488  cdleme32snaw  41586  cdleme32fvcl  41591  cdleme32le  41598  cdlemeg46gf  41684  cdleme48gfv  41688  cdleme50trn12  41703  cdlemg6  41774  cdlemg7N  41777  cdlemg38  41866  cdlemg46  41886  dibvalrel  42314  dihlss  42401  dihglblem5aN  42443  dihmeetbN  42454  dihmeetALTN  42478  dihatlat  42485  dihatexv  42489  dvh3dim2  42599  dvh3dim3N  42600  lclkrlem2h  42665  mapdh8d  42934  mapdh8g  42936  hdmap11lem2  42993  lcmineqlem23  43195  aks4d1p3  43222  aks4d1p5  43224  aks4d1p7d1  43226  posbezout  43244  aks6d1c2p2  43263  aks6d1c4  43268  aks6d1c5lem1  43280  aks6d1c6lem3  43316  aks6d1c6lem4  43317  bcled  43322  bcle2d  43323  aks6d1c7  43328  grpods  43338  unitscyglem2  43340  unitscyglem4  43342  aks5lem8  43345  dffltz  43764  ttac  44137  pw2f1ocnv  44138  aomclem5  44154  isnumbasgrplem3  44201  iocmbl  44309  oe0suclim  44373  tfsconcatfv  44437  safesnsupfidom1o  44512  safesnsupfilb  44513  r1rankcld  45323  grur1cld  45324  grucollcld  45338  mnuprd  45354  radcnvrat  45392  bccbc  45423  binomcxp  45435  fnchoice  46140  fiiuncl  46176  eliin2f  46213  founiiun0  46299  axccdom  46329  axccd2  46336  fzisoeu  46410  fperiodmul  46414  upbdrech2  46418  fzdifsuc2  46420  uzfissfz  46432  supxrgere  46439  supxrgelem  46443  supxrge  46444  suplesup  46445  infrpge  46457  xrlexaddrp  46458  xralrple2  46460  infxr  46472  infleinflem1  46475  infleinflem2  46476  infleinf  46477  xralrple3  46479  xrralrecnnge  46495  uzublem  46534  supxrmnf2  46537  infxrpnf  46550  infxrpnf2  46567  supminfxr  46568  supminfxr2  46573  pimxrneun  46592  rexanuz2nf  46596  ioondisj2  46599  iccdifprioo  46622  fmul01lt1lem1  46690  fmul01lt1lem2  46691  limciccioolb  46727  lptioo2  46737  lptioo1  46738  limcicciooub  46741  lptre2pt  46744  limcresiooub  46746  limcresioolb  46747  limcleqr  46748  climfveq  46773  climfveqf  46784  limsupubuzlem  46816  limsupubuz  46817  limsupmnfuzlem  46830  limsupre3uzlem  46839  climxrre  46854  limsup10exlem  46876  cnrefiisplem  46933  climxlim2lem  46949  dfxlim2v  46951  xlimliminflimsup  46966  coskpi2  46970  cosknegpi  46973  icccncfext  46991  cncfiooicclem1  46997  cncfiooicc  46998  cncfiooiccre  46999  dvbdfbdioolem2  47033  ioodvbdlimc1lem1  47035  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  dvnxpaek  47046  dvnprodlem1  47050  dvnprodlem3  47052  volioc  47076  itgioocnicc  47081  iblcncfioo  47082  volico  47087  sublevolico  47088  ismbl3  47090  ovolsplit  47092  volioore  47094  voliooico  47096  voliccico  47103  stoweidlem14  47118  stoweidlem26  47130  stoweidlem28  47132  stoweidlem55  47159  stoweid  47167  stirlinglem5  47182  stirlinglem12  47189  dirkerper  47200  dirkertrigeqlem3  47204  dirkertrigeq  47205  dirkercncflem1  47207  dirkercncflem2  47208  dirkercncf  47211  fourierdlem10  47221  fourierdlem12  47223  fourierdlem24  47235  fourierdlem30  47241  fourierdlem31  47242  fourierdlem32  47243  fourierdlem33  47244  fourierdlem34  47245  fourierdlem35  47246  fourierdlem37  47248  fourierdlem40  47251  fourierdlem41  47252  fourierdlem42  47253  fourierdlem43  47254  fourierdlem44  47255  fourierdlem46  47256  fourierdlem48  47258  fourierdlem49  47259  fourierdlem51  47261  fourierdlem54  47264  fourierdlem62  47272  fourierdlem64  47274  fourierdlem65  47275  fourierdlem70  47280  fourierdlem71  47281  fourierdlem73  47283  fourierdlem74  47284  fourierdlem75  47285  fourierdlem78  47288  fourierdlem79  47289  fourierdlem80  47290  fourierdlem81  47291  fourierdlem82  47292  fourierdlem92  47302  fourierdlem93  47303  fourierdlem97  47307  fourierdlem101  47311  fourierdlem102  47312  fourierdlem103  47313  fourierdlem104  47314  fourierdlem109  47319  fourierdlem114  47324  sqwvfoura  47332  sqwvfourb  47333  fourierswlem  47334  fouriersw  47335  elaa2lem  47337  etransclem15  47353  etransclem19  47357  etransclem20  47358  etransclem22  47360  etransclem23  47361  etransclem24  47362  etransclem25  47363  etransclem27  47365  etransclem28  47366  etransclem35  47373  etransclem38  47376  qndenserrnbl  47399  ioorrnopn  47409  ioorrnopnxrlem  47410  ioorrnopnxr  47411  prsal  47422  salexct  47438  issalnnd  47449  sge0sn  47483  sge0tsms  47484  sge0cl  47485  sge0f1o  47486  sge0sup  47495  sge0less  47496  sge0pr  47498  sge0prle  47505  sge0le  47511  sge0split  47513  sge0splitmpt  47515  sge0iunmptlemfi  47517  sge0iunmpt  47522  sge0isum  47531  sge0xaddlem1  47537  sge0xadd  47539  sge0gtfsumgt  47547  nnfoctbdjlem  47559  iundjiun  47564  meadjun  47566  ismeannd  47571  voliunsge0lem  47576  meaiuninc3v  47588  caragenfiiuncl  47619  omeiunltfirp  47623  carageniuncl  47627  caragenunicl  47628  isomenndlem  47634  isomennd  47635  hoicvr  47652  ovnssle  47665  ovn0  47670  ovnsubadd  47676  hsphoidmvle2  47689  hoidmvval0b  47694  hoidmv1lelem1  47695  hoidmv1lelem2  47696  hoidmv1le  47698  hoidmvlelem2  47700  hoidmvlelem3  47701  hoidmvlelem5  47703  hoidmvle  47704  ovnhoilem1  47705  ovnhoi  47707  ovnlecvr2  47714  hspdifhsp  47720  hoidifhspdmvle  47724  hoiqssbl  47729  hspmbllem1  47730  hspmbllem2  47731  hspmbl  47733  hoimbl  47735  volico2  47745  ovolval2lem  47747  ovnsubadd2lem  47749  ovolval4lem1  47753  ovolval4lem2  47754  ovolval5lem1  47756  vonhoire  47776  iunhoiioo  47780  vonioo  47786  vonicc  47789  vonsn  47795  pimrecltpos  47812  incsmflem  47845  smfpimltxr  47851  smfconst  47853  decsmflem  47870  smfpimgtxr  47884  smfrec  47893  smfpimne2  47944  sharhght  47969  tmachlem-agreeprod  48041  rrx2linest  49948  mofsn2  50050  ipolub00  50201  resccat  50282  initopropdlemlem  50455  prcof1  50617  parcoval2  50860  parmapcl  50865