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  2501  sbal2  2531  pm2.61danel  3057  ifeq1da  4561  ifeq2da  4562  ifeq12da  4563  ifclda  4565  ifeqda  4566  ifbothda  4568  2if2  4585  somin1  6155  xpcan  6197  fvmpti  7014  fvmptss  7027  funressn  7178  ovima0  7611  ordsuci  7827  suppssov1  8220  suppssov2  8221  oeoa  8633  oeoe  8635  omabs  8687  eceqoveq  8860  domdifsn  9092  pw2f1olem  9114  mapdom1  9180  imafiOLD  9351  marypha1lem  9470  supval2  9492  infdifsn  9694  ttrcltr  9753  ttrclselem1  9762  carden2b  10004  fidomtri  10030  dfac12lem2  10182  infunsdom1  10249  infunsdom  10250  itunisuc  10456  gchdomtri  10666  fiminre2  12213  xrmax2  13214  xrmin1  13215  ifle  13235  xnn0lem1lt  13282  xmulneg1  13307  xrsupsslem  13345  xrinfmsslem  13346  fzneuz  13644  seqf1olem1  14078  bccmpl  14344  bcval5  14353  bcpasc  14356  bccl  14357  hasheni  14383  hashfn  14410  hashdom  14414  hashdomi  14415  hashge1  14424  hashbc  14488  pfxval0  14710  sumz  15754  sumss  15756  fsumsplitsn  15776  sumsplit  15800  prod1  15976  prodss  15979  fprodsplitsn  16021  fprodle  16028  bitsmod  16469  sadadd2lem2  16483  sadcaddlem  16490  gcddvds  16536  gcdcl  16539  gcdneg  16555  dvdslcm  16631  lcmcl  16634  lcmneg  16636  lcmgcd  16640  lcmfcl  16661  dvdslcmf  16664  pcgcd  16911  pcmpt  16925  pcmpt2  16926  pcprod  16928  fldivp1  16930  prmreclem4  16952  vdwlem6  17019  ramub1lem1  17059  cidpropd  17754  rescabs  17882  rescabsOLD  17883  lubval  18413  glbval  18426  joinval  18434  meetval  18448  acsexdimd  18616  gsumpropd2lem  18704  gsumval2  18711  mulgfval  19099  f1otrspeq  19479  pmtrfinv  19493  psgnunilem1  19525  gsumval3  19939  ablfac1c  20105  ablfac1eu  20107  mgpress  20166  mgpressOLD  20167  frlmsslsp  21833  psrbas  21970  resspsrbas  22011  mplmonmul  22071  mplcoe1  22072  mplcoe5  22075  opsrle  22082  opsrbaslem  22084  opsrbaslemOLD  22085  psrbaspropd  22251  mplbaspropd  22253  mdetdiag  22620  mdetunilem7  22639  mdetunilem9  22641  maducoeval2  22661  madurid  22665  opnnei  23143  restbas  23181  hauspwdom  23524  ptcmplem5  24079  xrsmopn  24847  xrhmeo  24990  lebnum  25009  pcoass  25070  pcorevlem  25072  icombl  25612  ioombl  25613  mbfconstlem  25675  mbfima  25678  i1fd  25729  mbfi1fseqlem5  25768  itg2const2  25790  itg2seq  25791  itg2uba  25792  itg2splitlem  25797  itg2split  25798  itg2monolem1  25799  itg2gt0  25809  itg2cnlem1  25810  itg2cnlem2  25811  iblss  25854  iblss2  25855  itgss  25861  bddmulibl  25888  coemullem  26303  aaliou2b  26397  isppw2  27172  mule1  27205  ppip1le  27218  dchrelbas3  27296  dchrpt  27325  bposlem3  27344  bposlem5  27346  bposlem6  27347  lgslem4  27358  lgsneg  27379  lgsmod  27381  lgsdilem  27382  lgsdir  27390  lgsdi  27392  lgsne0  27393  lgsquad3  27445  dchrvmasum2if  27555  maxs2  27825  mins1  27826  midexlem  28714  colperpex  28755  outpasch  28777  hlpasch  28778  lnopp2hpgb  28785  lmieu  28806  inaghl  28867  cgrg3col4  28875  pthdlem1  29798  nmcfnlbi  32080  elpreq  32555  disjdifprg  32594  disjun0  32614  f1ocnt  32809  xrge0npcan  33007  psgnfzto1stlem  33102  cyc3genpmlem  33153  cyc3conja  33159  archiabl  33187  erlval  33244  orngsqr  33313  1arithufdlem3  33553  1arithufd  33555  resssra  33616  1smat1  33764  esumcst  34043  esumrnmpt2  34048  hasheuni  34065  esumcvg  34066  ddemeas  34216  omssubadd  34281  eulerpartlemgc  34343  eulerpartlemb  34349  plymulx  34541  signswmnd  34550  pthhashvtx  35111  erdsze2lem1  35187  mrsubvrs  35506  unblimceq0lem  36488  unbdqndv2lem2  36492  knoppndvlem10  36503  wl-spae  37501  wl-cbvalnaed  37512  wl-nfeqfb  37516  unccur  37589  poimirlem15  37621  poimirlem22  37628  itg2addnclem  37657  itg2addnclem2  37658  iblmulc2nc  37671  ftc1anclem5  37683  ftc1anc  37687  dvasin  37690  areacirclem5  37698  exmid2  38085  3dim1  39449  3dim2  39450  3dim3  39451  3atlem3  39467  3atlem7  39471  lvolnle3at  39564  2lplnja  39601  paddasslem18  39819  lhpexle3lem  39993  4atex  40058  cdlemd5  40184  cdleme16  40267  cdleme20  40306  cdleme21j  40318  cdleme21  40319  cdleme32snaw  40417  cdleme32fvcl  40422  cdleme32le  40429  cdlemeg46gf  40515  cdleme48gfv  40519  cdleme50trn12  40534  cdlemg6  40605  cdlemg7N  40608  cdlemg38  40697  cdlemg46  40717  dibvalrel  41145  dihlss  41232  dihglblem5aN  41274  dihmeetbN  41285  dihmeetALTN  41309  dihatlat  41316  dihatexv  41320  dvh3dim2  41430  dvh3dim3N  41431  lclkrlem2h  41496  mapdh8d  41765  mapdh8g  41767  hdmap11lem2  41824  lcmineqlem23  42032  aks4d1p3  42059  aks4d1p5  42061  aks4d1p7d1  42063  posbezout  42081  aks6d1c2p2  42100  aks6d1c4  42105  aks6d1c5lem1  42117  aks6d1c6lem3  42153  aks6d1c6lem4  42154  bcled  42159  bcle2d  42160  aks6d1c7  42165  grpods  42175  unitscyglem2  42177  unitscyglem4  42179  aks5lem8  42182  metakunt23  42208  metakunt24  42209  metakunt29  42214  metakunt30  42215  metakunt31  42216  dffltz  42620  ttac  43024  pw2f1ocnv  43025  aomclem5  43046  isnumbasgrplem3  43093  iocmbl  43201  oe0suclim  43266  tfsconcatfv  43330  safesnsupfidom1o  43406  safesnsupfilb  43407  r1rankcld  44226  grur1cld  44227  grucollcld  44255  mnuprd  44271  radcnvrat  44309  bccbc  44340  binomcxp  44352  fnchoice  44966  fiiuncl  45004  eliin2f  45043  founiiun0  45132  axccdom  45164  axccd2  45172  fzisoeu  45250  fperiodmul  45254  upbdrech2  45258  fzdifsuc2  45260  uzfissfz  45275  supxrgere  45282  supxrgelem  45286  supxrge  45287  suplesup  45288  infrpge  45300  xrlexaddrp  45301  xralrple2  45303  infxr  45316  infleinflem1  45319  infleinflem2  45320  infleinf  45321  xralrple3  45323  xrralrecnnge  45339  uzublem  45379  supxrmnf2  45382  infxrpnf  45395  infxrpnf2  45412  supminfxr  45413  supminfxr2  45418  pimxrneun  45438  rexanuz2nf  45442  ioondisj2  45445  iccdifprioo  45468  fmul01lt1lem1  45539  fmul01lt1lem2  45540  limciccioolb  45576  lptioo2  45586  lptioo1  45587  limcicciooub  45592  lptre2pt  45595  limcresiooub  45597  limcresioolb  45598  limcleqr  45599  climfveq  45624  climfveqf  45635  limsupubuzlem  45667  limsupubuz  45668  limsupmnfuzlem  45681  limsupre3uzlem  45690  climxrre  45705  limsup10exlem  45727  cnrefiisplem  45784  climxlim2lem  45800  dfxlim2v  45802  xlimliminflimsup  45817  coskpi2  45821  cosknegpi  45824  icccncfext  45842  cncfiooicclem1  45848  cncfiooicc  45849  cncfiooiccre  45850  dvbdfbdioolem2  45884  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnxpaek  45897  dvnprodlem1  45901  dvnprodlem3  45903  volioc  45927  itgioocnicc  45932  iblcncfioo  45933  volico  45938  sublevolico  45939  ismbl3  45941  ovolsplit  45943  volioore  45945  voliooico  45947  voliccico  45954  stoweidlem14  45969  stoweidlem26  45981  stoweidlem28  45983  stoweidlem55  46010  stoweid  46018  stirlinglem5  46033  stirlinglem12  46040  dirkerper  46051  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkercncflem1  46058  dirkercncflem2  46059  dirkercncf  46062  fourierdlem10  46072  fourierdlem12  46074  fourierdlem24  46086  fourierdlem30  46092  fourierdlem31  46093  fourierdlem32  46094  fourierdlem33  46095  fourierdlem34  46096  fourierdlem35  46097  fourierdlem37  46099  fourierdlem40  46102  fourierdlem41  46103  fourierdlem42  46104  fourierdlem43  46105  fourierdlem44  46106  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem51  46112  fourierdlem54  46115  fourierdlem62  46123  fourierdlem64  46125  fourierdlem65  46126  fourierdlem70  46131  fourierdlem71  46132  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem78  46139  fourierdlem79  46140  fourierdlem80  46141  fourierdlem81  46142  fourierdlem82  46143  fourierdlem92  46153  fourierdlem93  46154  fourierdlem97  46158  fourierdlem101  46162  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem109  46170  fourierdlem114  46175  sqwvfoura  46183  sqwvfourb  46184  fourierswlem  46185  fouriersw  46186  elaa2lem  46188  etransclem15  46204  etransclem19  46208  etransclem20  46209  etransclem22  46211  etransclem23  46212  etransclem24  46213  etransclem25  46214  etransclem27  46216  etransclem28  46217  etransclem35  46224  etransclem38  46227  qndenserrnbl  46250  ioorrnopn  46260  ioorrnopnxrlem  46261  ioorrnopnxr  46262  prsal  46273  salexct  46289  issalnnd  46300  sge0sn  46334  sge0tsms  46335  sge0cl  46336  sge0f1o  46337  sge0sup  46346  sge0less  46347  sge0pr  46349  sge0prle  46356  sge0le  46362  sge0split  46364  sge0splitmpt  46366  sge0iunmptlemfi  46368  sge0iunmpt  46373  sge0isum  46382  sge0xaddlem1  46388  sge0xadd  46390  sge0gtfsumgt  46398  nnfoctbdjlem  46410  iundjiun  46415  meadjun  46417  ismeannd  46422  voliunsge0lem  46427  meaiuninc3v  46439  caragenfiiuncl  46470  omeiunltfirp  46474  carageniuncl  46478  caragenunicl  46479  isomenndlem  46485  isomennd  46486  hoicvr  46503  ovnssle  46516  ovn0  46521  ovnsubadd  46527  hsphoidmvle2  46540  hoidmvval0b  46545  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1le  46549  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem5  46554  hoidmvle  46555  ovnhoilem1  46556  ovnhoi  46558  ovnlecvr2  46565  hspdifhsp  46571  hoidifhspdmvle  46575  hoiqssbl  46580  hspmbllem1  46581  hspmbllem2  46582  hspmbl  46584  hoimbl  46586  volico2  46596  ovolval2lem  46598  ovnsubadd2lem  46600  ovolval4lem1  46604  ovolval4lem2  46605  ovolval5lem1  46607  vonhoire  46627  iunhoiioo  46631  vonioo  46637  vonicc  46640  vonsn  46646  pimrecltpos  46663  incsmflem  46696  smfpimltxr  46702  smfconst  46704  decsmflem  46721  smfpimgtxr  46735  smfrec  46744  smfpimne2  46795  sharhght  46820  rrx2linest  48591  mofsn2  48674  ipolub00  48781