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  2529  sbal2  2559  pm2.61danel  3076  ifeq1da  4514  ifeq2da  4515  ifeq12da  4516  ifclda  4518  ifeqda  4519  ifbothda  4521  2if2  4538  somin1  6127  xpcan  6168  fvmpti  6990  fvmptss  7004  funressn  7161  ovima0  7598  ordsuci  7820  suppssov1  8207  suppssov2  8208  oeoa  8599  oeoe  8601  omabs  8653  eceqoveq  8836  domdifsn  9072  pw2f1olem  9093  mapdom1  9154  marypha1lem  9418  supval2  9440  infdifsn  9651  ttrcltr  9710  ttrclselem1  9719  carden2b  10041  fidomtri  10067  dfac12lem2  10216  infunsdom1  10283  infunsdom  10284  itunisuc  10490  gchdomtri  10707  fiminre2  12258  xrmax2  13299  xrmin1  13300  ifle  13320  xnn0lem1lt  13367  xmulneg1  13392  xrsupsslem  13430  xrinfmsslem  13431  fzneuz  13735  seqf1olem1  14177  bccmpl  14446  bcval5  14455  bcpasc  14458  bccl  14459  hasheni  14485  hashfn  14512  hashdom  14516  hashdomi  14517  hashge1  14526  hashbc  14591  pfxval0  14819  sumz  15881  sumss  15883  fsumsplitsn  15903  sumsplit  15927  prod1  16104  prodss  16107  fprodsplitsn  16149  fprodle  16156  bitsmod  16599  sadadd2lem2  16613  sadcaddlem  16620  gcddvds  16666  gcdcl  16669  gcdneg  16687  dvdslcm  16766  lcmcl  16769  lcmneg  16771  lcmgcd  16775  lcmfcl  16796  dvdslcmf  16799  pcgcd  17049  pcmpt  17063  pcmpt2  17064  pcprod  17066  fldivp1  17068  prmreclem4  17090  vdwlem6  17157  ramub1lem1  17197  cidpropd  17877  rescabs  18001  lubval  18521  glbval  18534  joinval  18542  meetval  18556  acsexdimd  18726  gsumpropd2lem  18861  gsumval2  18868  mulgfval  19272  f1otrspeq  19654  pmtrfinv  19668  psgnunilem1  19700  gsumval3  20114  ablfac1c  20280  ablfac1eu  20282  mgpress  20363  orngsqr  21116  frlmsslsp  22095  psrbas  22235  resspsrbas  22274  mplmonmul  22338  mplcoe1  22339  mplcoe5  22342  opsrle  22349  opsrbaslem  22351  psrbaspropd  22545  mplbaspropd  22547  mdetdiag  22907  mdetunilem7  22926  mdetunilem9  22928  maducoeval2  22948  madurid  22952  opnnei  23431  restbas  23469  hauspwdom  23813  ptcmplem5  24368  xrsmopn  25125  xrhmeo  25260  lebnum  25278  pcoass  25338  pcorevlem  25340  icombl  25878  ioombl  25879  mbfconstlem  25941  mbfima  25944  i1fd  25995  mbfi1fseqlem5  26033  itg2const2  26055  itg2seq  26056  itg2uba  26057  itg2splitlem  26062  itg2split  26063  itg2monolem1  26064  itg2gt0  26074  itg2cnlem1  26075  itg2cnlem2  26076  iblss  26118  iblss2  26119  itgss  26125  bddmulibl  26152  coemullem  26562  plymulidp  26596  aaliou2b  26661  isppw2  27435  mule1  27468  ppip1le  27481  dchrelbas3  27558  dchrpt  27587  bposlem3  27606  bposlem5  27608  bposlem6  27609  lgslem4  27620  lgsneg  27641  lgsmod  27643  lgsdilem  27644  lgsdir  27652  lgsdi  27654  lgsne0  27655  lgsquad3  27707  dchrvmasum2if  27817  maxs2  28120  mins1  28121  z12bday  28864  tglnpt4  29116  midexlem  29157  colperpex  29202  outpasch  29226  hlpasch  29227  lnopp2hpgb  29234  lmieu  29282  perpeq  29341  tgaaddcpbl  29345  inaghl  29357  cgrg3col4  29365  angmgmaddov1lem  29379  angmgmaddrid  29386  perpprlng  29421  prlngex  29422  prlngmo2  29427  pthhashvtx  30308  pthdlem1  30345  nmcfnlbi  32647  elpreq  33117  prssad  33118  prssbd  33119  disjdifprg  33162  disjun0  33182  argcj  33333  f1ocnt  33385  xrge0npcan  33574  psgnfzto1stlem  33654  cyc3genpmlem  33705  cyc3conja  33711  archiabl  33752  erlval  33812  1arithufdlem3  34071  1arithufd  34073  psrmonmul  34175  esplyfval3  34197  resssra  34212  lbslelsp  34223  constrrecl  34394  constrinvcl  34398  constrsqrtcl  34404  1smat1  34429  esumcst  34688  esumrnmpt2  34693  hasheuni  34710  esumcvg  34711  ddemeas  34862  omssubadd  34925  eulerpartlemgc  34987  eulerpartlemb  34993  signswmnd  35179  fineqvnttrclselem1  35772  erdsze2lem1  35947  mrsubvrs  36266  unblimceq0lem  37352  unbdqndv2lem2  37356  knoppndvlem10  37367  wl-spae  38433  wl-cbvalnaed  38444  wl-nfeqfb  38448  unccur  38506  poimirlem15  38533  poimirlem22  38540  itg2addnclem  38569  itg2addnclem2  38570  iblmulc2nc  38583  ftc1anclem5  38595  ftc1anc  38599  dvasin  38602  areacirclem5  38610  exmid2  39011  3dim1  40504  3dim2  40505  3dim3  40506  3atlem3  40522  3atlem7  40526  lvolnle3at  40619  2lplnja  40656  paddasslem18  40874  lhpexle3lem  41048  4atex  41113  cdlemd5  41239  cdleme16  41322  cdleme20  41361  cdleme21j  41373  cdleme21  41374  cdleme32snaw  41472  cdleme32fvcl  41477  cdleme32le  41484  cdlemeg46gf  41570  cdleme48gfv  41574  cdleme50trn12  41589  cdlemg6  41660  cdlemg7N  41663  cdlemg38  41752  cdlemg46  41772  dibvalrel  42200  dihlss  42287  dihglblem5aN  42329  dihmeetbN  42340  dihmeetALTN  42364  dihatlat  42371  dihatexv  42375  dvh3dim2  42485  dvh3dim3N  42486  lclkrlem2h  42551  mapdh8d  42820  mapdh8g  42822  hdmap11lem2  42879  lcmineqlem23  43081  aks4d1p3  43108  aks4d1p5  43110  aks4d1p7d1  43112  posbezout  43130  aks6d1c2p2  43149  aks6d1c4  43154  aks6d1c5lem1  43166  aks6d1c6lem3  43202  aks6d1c6lem4  43203  bcled  43208  bcle2d  43209  aks6d1c7  43214  grpods  43224  unitscyglem2  43226  unitscyglem4  43228  aks5lem8  43231  dffltz  43650  ttac  44022  pw2f1ocnv  44023  aomclem5  44044  isnumbasgrplem3  44091  iocmbl  44199  oe0suclim  44263  tfsconcatfv  44327  safesnsupfidom1o  44402  safesnsupfilb  44403  r1rankcld  45214  grur1cld  45215  grucollcld  45229  mnuprd  45245  radcnvrat  45283  bccbc  45314  binomcxp  45326  fnchoice  46015  fiiuncl  46051  eliin2f  46088  founiiun0  46174  axccdom  46204  axccd2  46211  fzisoeu  46285  fperiodmul  46289  upbdrech2  46293  fzdifsuc2  46295  uzfissfz  46307  supxrgere  46314  supxrgelem  46318  supxrge  46319  suplesup  46320  infrpge  46332  xrlexaddrp  46333  xralrple2  46335  infxr  46347  infleinflem1  46350  infleinflem2  46351  infleinf  46352  xralrple3  46354  xrralrecnnge  46370  uzublem  46409  supxrmnf2  46412  infxrpnf  46425  infxrpnf2  46442  supminfxr  46443  supminfxr2  46448  pimxrneun  46467  rexanuz2nf  46471  ioondisj2  46474  iccdifprioo  46497  fmul01lt1lem1  46565  fmul01lt1lem2  46566  limciccioolb  46602  lptioo2  46612  lptioo1  46613  limcicciooub  46616  lptre2pt  46619  limcresiooub  46621  limcresioolb  46622  limcleqr  46623  climfveq  46648  climfveqf  46659  limsupubuzlem  46691  limsupubuz  46692  limsupmnfuzlem  46705  limsupre3uzlem  46714  climxrre  46729  limsup10exlem  46751  cnrefiisplem  46808  climxlim2lem  46824  dfxlim2v  46826  xlimliminflimsup  46841  coskpi2  46845  cosknegpi  46848  icccncfext  46866  cncfiooicclem1  46872  cncfiooicc  46873  cncfiooiccre  46874  dvbdfbdioolem2  46908  ioodvbdlimc1lem1  46910  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  dvnxpaek  46921  dvnprodlem1  46925  dvnprodlem3  46927  volioc  46951  itgioocnicc  46956  iblcncfioo  46957  volico  46962  sublevolico  46963  ismbl3  46965  ovolsplit  46967  volioore  46969  voliooico  46971  voliccico  46978  stoweidlem14  46993  stoweidlem26  47005  stoweidlem28  47007  stoweidlem55  47034  stoweid  47042  stirlinglem5  47057  stirlinglem12  47064  dirkerper  47075  dirkertrigeqlem3  47079  dirkertrigeq  47080  dirkercncflem1  47082  dirkercncflem2  47083  dirkercncf  47086  fourierdlem10  47096  fourierdlem12  47098  fourierdlem24  47110  fourierdlem30  47116  fourierdlem31  47117  fourierdlem32  47118  fourierdlem33  47119  fourierdlem34  47120  fourierdlem35  47121  fourierdlem37  47123  fourierdlem40  47126  fourierdlem41  47127  fourierdlem42  47128  fourierdlem43  47129  fourierdlem44  47130  fourierdlem46  47131  fourierdlem48  47133  fourierdlem49  47134  fourierdlem51  47136  fourierdlem54  47139  fourierdlem62  47147  fourierdlem64  47149  fourierdlem65  47150  fourierdlem70  47155  fourierdlem71  47156  fourierdlem73  47158  fourierdlem74  47159  fourierdlem75  47160  fourierdlem78  47163  fourierdlem79  47164  fourierdlem80  47165  fourierdlem81  47166  fourierdlem82  47167  fourierdlem92  47177  fourierdlem93  47178  fourierdlem97  47182  fourierdlem101  47186  fourierdlem102  47187  fourierdlem103  47188  fourierdlem104  47189  fourierdlem109  47194  fourierdlem114  47199  sqwvfoura  47207  sqwvfourb  47208  fourierswlem  47209  fouriersw  47210  elaa2lem  47212  etransclem15  47228  etransclem19  47232  etransclem20  47233  etransclem22  47235  etransclem23  47236  etransclem24  47237  etransclem25  47238  etransclem27  47240  etransclem28  47241  etransclem35  47248  etransclem38  47251  qndenserrnbl  47274  ioorrnopn  47284  ioorrnopnxrlem  47285  ioorrnopnxr  47286  prsal  47297  salexct  47313  issalnnd  47324  sge0sn  47358  sge0tsms  47359  sge0cl  47360  sge0f1o  47361  sge0sup  47370  sge0less  47371  sge0pr  47373  sge0prle  47380  sge0le  47386  sge0split  47388  sge0splitmpt  47390  sge0iunmptlemfi  47392  sge0iunmpt  47397  sge0isum  47406  sge0xaddlem1  47412  sge0xadd  47414  sge0gtfsumgt  47422  nnfoctbdjlem  47434  iundjiun  47439  meadjun  47441  ismeannd  47446  voliunsge0lem  47451  meaiuninc3v  47463  caragenfiiuncl  47494  omeiunltfirp  47498  carageniuncl  47502  caragenunicl  47503  isomenndlem  47509  isomennd  47510  hoicvr  47527  ovnssle  47540  ovn0  47545  ovnsubadd  47551  hsphoidmvle2  47564  hoidmvval0b  47569  hoidmv1lelem1  47570  hoidmv1lelem2  47571  hoidmv1le  47573  hoidmvlelem2  47575  hoidmvlelem3  47576  hoidmvlelem5  47578  hoidmvle  47579  ovnhoilem1  47580  ovnhoi  47582  ovnlecvr2  47589  hspdifhsp  47595  hoidifhspdmvle  47599  hoiqssbl  47604  hspmbllem1  47605  hspmbllem2  47606  hspmbl  47608  hoimbl  47610  volico2  47620  ovolval2lem  47622  ovnsubadd2lem  47624  ovolval4lem1  47628  ovolval4lem2  47629  ovolval5lem1  47631  vonhoire  47651  iunhoiioo  47655  vonioo  47661  vonicc  47664  vonsn  47670  pimrecltpos  47687  incsmflem  47720  smfpimltxr  47726  smfconst  47728  decsmflem  47745  smfpimgtxr  47759  smfrec  47768  smfpimne2  47819  sharhght  47844  tmachlem-agreeprod  47916  rrx2linest  49823  mofsn2  49924  ipolub00  50070  resccat  50151  initopropdlemlem  50316  prcof1  50465