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  2534  sbal2  2564  pm2.61danel  3081  ifeq1da  4524  ifeq2da  4525  ifeq12da  4526  ifclda  4528  ifeqda  4529  ifbothda  4531  2if2  4548  somin1  6138  xpcan  6179  fvmpti  6995  fvmptss  7009  funressn  7163  ovima0  7602  ordsuci  7816  suppssov1  8202  suppssov2  8203  oeoa  8592  oeoe  8594  omabs  8646  eceqoveq  8829  domdifsn  9058  pw2f1olem  9079  mapdom1  9140  marypha1lem  9403  supval2  9425  infdifsn  9636  ttrcltr  9695  ttrclselem1  9704  carden2b  9972  fidomtri  9998  dfac12lem2  10147  infunsdom1  10214  infunsdom  10215  itunisuc  10421  gchdomtri  10632  fiminre2  12181  xrmax2  13220  xrmin1  13221  ifle  13241  xnn0lem1lt  13288  xmulneg1  13313  xrsupsslem  13351  xrinfmsslem  13352  fzneuz  13655  seqf1olem1  14097  bccmpl  14365  bcval5  14374  bcpasc  14377  bccl  14378  hasheni  14404  hashfn  14431  hashdom  14435  hashdomi  14436  hashge1  14445  hashbc  14510  pfxval0  14738  sumz  15799  sumss  15801  fsumsplitsn  15821  sumsplit  15845  prod1  16024  prodss  16027  fprodsplitsn  16069  fprodle  16076  bitsmod  16519  sadadd2lem2  16533  sadcaddlem  16540  gcddvds  16586  gcdcl  16589  gcdneg  16605  dvdslcm  16681  lcmcl  16684  lcmneg  16686  lcmgcd  16690  lcmfcl  16711  dvdslcmf  16714  pcgcd  16963  pcmpt  16977  pcmpt2  16978  pcprod  16980  fldivp1  16982  prmreclem4  17004  vdwlem6  17071  ramub1lem1  17111  cidpropd  17791  rescabs  17915  lubval  18435  glbval  18448  joinval  18456  meetval  18470  acsexdimd  18640  gsumpropd2lem  18766  gsumval2  18773  mulgfval  19166  f1otrspeq  19548  pmtrfinv  19562  psgnunilem1  19594  gsumval3  20008  ablfac1c  20174  ablfac1eu  20176  mgpress  20257  orngsqr  21006  frlmsslsp  21983  psrbas  22121  resspsrbas  22160  mplmonmul  22224  mplcoe1  22225  mplcoe5  22228  opsrle  22235  opsrbaslem  22237  psrbaspropd  22431  mplbaspropd  22433  mdetdiag  22793  mdetunilem7  22812  mdetunilem9  22814  maducoeval2  22834  madurid  22838  opnnei  23314  restbas  23352  hauspwdom  23695  ptcmplem5  24250  xrsmopn  25007  xrhmeo  25142  lebnum  25160  pcoass  25220  pcorevlem  25222  icombl  25760  ioombl  25761  mbfconstlem  25823  mbfima  25826  i1fd  25877  mbfi1fseqlem5  25915  itg2const2  25937  itg2seq  25938  itg2uba  25939  itg2splitlem  25944  itg2split  25945  itg2monolem1  25946  itg2gt0  25956  itg2cnlem1  25957  itg2cnlem2  25958  iblss  26001  iblss2  26002  itgss  26008  bddmulibl  26035  coemullem  26444  plymulidp  26480  aaliou2b  26541  isppw2  27316  mule1  27349  ppip1le  27362  dchrelbas3  27439  dchrpt  27468  bposlem3  27487  bposlem5  27489  bposlem6  27490  lgslem4  27501  lgsneg  27522  lgsmod  27524  lgsdilem  27525  lgsdir  27533  lgsdi  27535  lgsne0  27536  lgsquad3  27588  dchrvmasum2if  27698  maxs2  27971  mins1  27972  z12bday  28715  tglnpt4  28965  midexlem  29006  colperpex  29051  outpasch  29074  hlpasch  29075  lnopp2hpgb  29082  lmieu  29130  perpeq  29188  inaghl  29199  cgrg3col4  29207  perpprlng  29237  prlngex  29238  prlngmo2  29243  pthdlem1  30152  nmcfnlbi  32441  elpreq  32911  prssad  32912  prssbd  32913  disjdifprg  32957  disjun0  32977  argcj  33130  f1ocnt  33182  xrge0npcan  33371  psgnfzto1stlem  33451  cyc3genpmlem  33502  cyc3conja  33508  archiabl  33549  erlval  33609  1arithufdlem3  33867  1arithufd  33869  psrmonmul  33971  esplyfval3  33993  resssra  34008  lbslelsp  34019  constrrecl  34190  constrinvcl  34194  constrsqrtcl  34200  1smat1  34225  esumcst  34484  esumrnmpt2  34489  hasheuni  34506  esumcvg  34507  ddemeas  34658  omssubadd  34722  eulerpartlemgc  34784  eulerpartlemb  34790  signswmnd  34976  fineqvnttrclselem1  35558  pthhashvtx  35641  erdsze2lem1  35716  mrsubvrs  36035  unblimceq0lem  37136  unbdqndv2lem2  37140  knoppndvlem10  37151  wl-spae  38217  wl-cbvalnaed  38228  wl-nfeqfb  38232  unccur  38295  poimirlem15  38327  poimirlem22  38334  itg2addnclem  38363  itg2addnclem2  38364  iblmulc2nc  38377  ftc1anclem5  38389  ftc1anc  38393  dvasin  38396  areacirclem5  38404  exmid2  38789  3dim1  40282  3dim2  40283  3dim3  40284  3atlem3  40300  3atlem7  40304  lvolnle3at  40397  2lplnja  40434  paddasslem18  40652  lhpexle3lem  40826  4atex  40891  cdlemd5  41017  cdleme16  41100  cdleme20  41139  cdleme21j  41151  cdleme21  41152  cdleme32snaw  41250  cdleme32fvcl  41255  cdleme32le  41262  cdlemeg46gf  41348  cdleme48gfv  41352  cdleme50trn12  41367  cdlemg6  41438  cdlemg7N  41441  cdlemg38  41530  cdlemg46  41550  dibvalrel  41978  dihlss  42065  dihglblem5aN  42107  dihmeetbN  42118  dihmeetALTN  42142  dihatlat  42149  dihatexv  42153  dvh3dim2  42263  dvh3dim3N  42264  lclkrlem2h  42329  mapdh8d  42598  mapdh8g  42600  hdmap11lem2  42657  lcmineqlem23  42859  aks4d1p3  42886  aks4d1p5  42888  aks4d1p7d1  42890  posbezout  42908  aks6d1c2p2  42927  aks6d1c4  42932  aks6d1c5lem1  42944  aks6d1c6lem3  42980  aks6d1c6lem4  42981  bcled  42986  bcle2d  42987  aks6d1c7  42992  grpods  43002  unitscyglem2  43004  unitscyglem4  43006  aks5lem8  43009  dffltz  43407  ttac  43804  pw2f1ocnv  43805  aomclem5  43826  isnumbasgrplem3  43873  iocmbl  43981  oe0suclim  44045  tfsconcatfv  44109  safesnsupfidom1o  44184  safesnsupfilb  44185  r1rankcld  44996  grur1cld  44997  grucollcld  45011  mnuprd  45027  radcnvrat  45065  bccbc  45096  binomcxp  45108  fnchoice  45790  fiiuncl  45826  eliin2f  45863  founiiun0  45949  axccdom  45979  axccd2  45986  fzisoeu  46060  fperiodmul  46064  upbdrech2  46068  fzdifsuc2  46070  uzfissfz  46083  supxrgere  46090  supxrgelem  46094  supxrge  46095  suplesup  46096  infrpge  46108  xrlexaddrp  46109  xralrple2  46111  infxr  46123  infleinflem1  46126  infleinflem2  46127  infleinf  46128  xralrple3  46130  xrralrecnnge  46146  uzublem  46185  supxrmnf2  46188  infxrpnf  46201  infxrpnf2  46218  supminfxr  46219  supminfxr2  46224  pimxrneun  46243  rexanuz2nf  46247  ioondisj2  46250  iccdifprioo  46273  fmul01lt1lem1  46341  fmul01lt1lem2  46342  limciccioolb  46378  lptioo2  46388  lptioo1  46389  limcicciooub  46392  lptre2pt  46395  limcresiooub  46397  limcresioolb  46398  limcleqr  46399  climfveq  46424  climfveqf  46435  limsupubuzlem  46467  limsupubuz  46468  limsupmnfuzlem  46481  limsupre3uzlem  46490  climxrre  46505  limsup10exlem  46527  cnrefiisplem  46584  climxlim2lem  46600  dfxlim2v  46602  xlimliminflimsup  46617  coskpi2  46621  cosknegpi  46624  icccncfext  46642  cncfiooicclem1  46648  cncfiooicc  46649  cncfiooiccre  46650  dvbdfbdioolem2  46684  ioodvbdlimc1lem1  46686  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  dvnxpaek  46697  dvnprodlem1  46701  dvnprodlem3  46703  volioc  46727  itgioocnicc  46732  iblcncfioo  46733  volico  46738  sublevolico  46739  ismbl3  46741  ovolsplit  46743  volioore  46745  voliooico  46747  voliccico  46754  stoweidlem14  46769  stoweidlem26  46781  stoweidlem28  46783  stoweidlem55  46810  stoweid  46818  stirlinglem5  46833  stirlinglem12  46840  dirkerper  46851  dirkertrigeqlem3  46855  dirkertrigeq  46856  dirkercncflem1  46858  dirkercncflem2  46859  dirkercncf  46862  fourierdlem10  46872  fourierdlem12  46874  fourierdlem24  46886  fourierdlem30  46892  fourierdlem31  46893  fourierdlem32  46894  fourierdlem33  46895  fourierdlem34  46896  fourierdlem35  46897  fourierdlem37  46899  fourierdlem40  46902  fourierdlem41  46903  fourierdlem42  46904  fourierdlem43  46905  fourierdlem44  46906  fourierdlem46  46907  fourierdlem48  46909  fourierdlem49  46910  fourierdlem51  46912  fourierdlem54  46915  fourierdlem62  46923  fourierdlem64  46925  fourierdlem65  46926  fourierdlem70  46931  fourierdlem71  46932  fourierdlem73  46934  fourierdlem74  46935  fourierdlem75  46936  fourierdlem78  46939  fourierdlem79  46940  fourierdlem80  46941  fourierdlem81  46942  fourierdlem82  46943  fourierdlem92  46953  fourierdlem93  46954  fourierdlem97  46958  fourierdlem101  46962  fourierdlem102  46963  fourierdlem103  46964  fourierdlem104  46965  fourierdlem109  46970  fourierdlem114  46975  sqwvfoura  46983  sqwvfourb  46984  fourierswlem  46985  fouriersw  46986  elaa2lem  46988  etransclem15  47004  etransclem19  47008  etransclem20  47009  etransclem22  47011  etransclem23  47012  etransclem24  47013  etransclem25  47014  etransclem27  47016  etransclem28  47017  etransclem35  47024  etransclem38  47027  qndenserrnbl  47050  ioorrnopn  47060  ioorrnopnxrlem  47061  ioorrnopnxr  47062  prsal  47073  salexct  47089  issalnnd  47100  sge0sn  47134  sge0tsms  47135  sge0cl  47136  sge0f1o  47137  sge0sup  47146  sge0less  47147  sge0pr  47149  sge0prle  47156  sge0le  47162  sge0split  47164  sge0splitmpt  47166  sge0iunmptlemfi  47168  sge0iunmpt  47173  sge0isum  47182  sge0xaddlem1  47188  sge0xadd  47190  sge0gtfsumgt  47198  nnfoctbdjlem  47210  iundjiun  47215  meadjun  47217  ismeannd  47222  voliunsge0lem  47227  meaiuninc3v  47239  caragenfiiuncl  47270  omeiunltfirp  47274  carageniuncl  47278  caragenunicl  47279  isomenndlem  47285  isomennd  47286  hoicvr  47303  ovnssle  47316  ovn0  47321  ovnsubadd  47327  hsphoidmvle2  47340  hoidmvval0b  47345  hoidmv1lelem1  47346  hoidmv1lelem2  47347  hoidmv1le  47349  hoidmvlelem2  47351  hoidmvlelem3  47352  hoidmvlelem5  47354  hoidmvle  47355  ovnhoilem1  47356  ovnhoi  47358  ovnlecvr2  47365  hspdifhsp  47371  hoidifhspdmvle  47375  hoiqssbl  47380  hspmbllem1  47381  hspmbllem2  47382  hspmbl  47384  hoimbl  47386  volico2  47396  ovolval2lem  47398  ovnsubadd2lem  47400  ovolval4lem1  47404  ovolval4lem2  47405  ovolval5lem1  47407  vonhoire  47427  iunhoiioo  47431  vonioo  47437  vonicc  47440  vonsn  47446  pimrecltpos  47463  incsmflem  47496  smfpimltxr  47502  smfconst  47504  decsmflem  47521  smfpimgtxr  47535  smfrec  47544  smfpimne2  47595  sharhght  47620  rrx2linest  49563  mofsn2  49664  ipolub00  49812  resccat  49893  initopropdlemlem  50058  prcof1  50207