Theorem pm2.61dan 812

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  pm2.61ddan  813  pm2.61dda  814  nfsb4t  2499  sbal2  2529  pm2.61danel  3061  ifeq1da  4560  ifeq2da  4561  ifeq12da  4562  ifclda  4564  ifeqda  4565  ifbothda  4567  2if2  4584  somin1  6135  xpcan  6176  fvmpti  6998  fvmptss  7011  funressn  7157  ovima0  7586  ordsuci  7796  oeoa  8597  oeoe  8599  omabs  8650  eceqoveq  8816  domdifsn  9054  pw2f1olem  9076  mapdom1  9142  imafi  9175  marypha1lem  9428  supval2  9450  infdifsn  9652  ttrcltr  9711  ttrclselem1  9720  carden2b  9962  fidomtri  9988  dfac12lem2  10139  infunsdom1  10208  infunsdom  10209  itunisuc  10414  gchdomtri  10624  fiminre2  12162  xrmax2  13155  xrmin1  13156  ifle  13176  xnn0lem1lt  13223  xmulneg1  13248  xrsupsslem  13286  xrinfmsslem  13287  fzneuz  13582  seqf1olem1  14007  bccmpl  14269  bcval5  14278  bcpasc  14281  bccl  14282  hasheni  14308  hashfn  14335  hashdom  14339  hashdomi  14340  hashge1  14349  hashbc  14412  pfxval0  14626  sumz  15668  sumss  15670  fsumsplitsn  15690  sumsplit  15714  prod1  15888  prodss  15891  fprodsplitsn  15933  fprodle  15940  bitsmod  16377  sadadd2lem2  16391  sadcaddlem  16398  gcddvds  16444  gcdcl  16447  gcdneg  16463  dvdslcm  16535  lcmcl  16538  lcmneg  16540  lcmgcd  16544  lcmfcl  16565  dvdslcmf  16568  pcgcd  16811  pcmpt  16825  pcmpt2  16826  pcprod  16828  fldivp1  16830  prmreclem4  16852  vdwlem6  16919  ramub1lem1  16959  cidpropd  17654  rescabs  17782  rescabsOLD  17783  lubval  18309  glbval  18322  joinval  18330  meetval  18344  acsexdimd  18512  gsumpropd2lem  18598  gsumval2  18605  mulgfval  18952  f1otrspeq  19315  pmtrfinv  19329  psgnunilem1  19361  gsumval3  19775  ablfac1c  19941  ablfac1eu  19943  mgpress  20002  mgpressOLD  20003  frlmsslsp  21351  psrbas  21497  resspsrbas  21535  mplmonmul  21591  mplcoe1  21592  mplcoe5  21595  opsrle  21602  opsrbaslem  21604  opsrbaslemOLD  21605  psrbaspropd  21757  mplbaspropd  21759  mdetdiag  22101  mdetunilem7  22120  mdetunilem9  22122  maducoeval2  22142  madurid  22146  opnnei  22624  restbas  22662  hauspwdom  23005  ptcmplem5  23560  xrsmopn  24328  xrhmeo  24462  lebnum  24480  pcoass  24540  pcorevlem  24542  icombl  25081  ioombl  25082  mbfconstlem  25144  mbfima  25147  i1fd  25198  mbfi1fseqlem5  25237  itg2const2  25259  itg2seq  25260  itg2uba  25261  itg2splitlem  25266  itg2split  25267  itg2monolem1  25268  itg2gt0  25278  itg2cnlem1  25279  itg2cnlem2  25280  iblss  25322  iblss2  25323  itgss  25329  bddmulibl  25356  coemullem  25764  aaliou2b  25854  isppw2  26619  mule1  26652  ppip1le  26665  dchrelbas3  26741  dchrpt  26770  bposlem3  26789  bposlem5  26791  bposlem6  26792  lgslem4  26803  lgsneg  26824  lgsmod  26826  lgsdilem  26827  lgsdir  26835  lgsdi  26837  lgsne0  26838  lgsquad3  26890  dchrvmasum2if  27000  maxs2  27269  mins1  27270  midexlem  27943  colperpex  27984  outpasch  28006  hlpasch  28007  lnopp2hpgb  28014  lmieu  28035  inaghl  28096  cgrg3col4  28104  pthdlem1  29023  nmcfnlbi  31305  elpreq  31767  disjdifprg  31806  disjun0  31826  f1ocnt  32013  xrge0npcan  32195  psgnfzto1stlem  32259  cyc3genpmlem  32310  cyc3conja  32316  archiabl  32344  orngsqr  32422  1smat1  32784  esumcst  33061  esumrnmpt2  33066  hasheuni  33083  esumcvg  33084  ddemeas  33234  omssubadd  33299  eulerpartlemgc  33361  eulerpartlemb  33367  plymulx  33559  signswmnd  33568  pthhashvtx  34118  erdsze2lem1  34194  mrsubvrs  34513  unblimceq0lem  35382  unbdqndv2lem2  35386  knoppndvlem10  35397  wl-spae  36390  wl-cbvalnaed  36401  wl-nfeqfb  36405  unccur  36471  poimirlem15  36503  poimirlem22  36510  itg2addnclem  36539  itg2addnclem2  36540  iblmulc2nc  36553  ftc1anclem5  36565  ftc1anc  36569  dvasin  36572  areacirclem5  36580  exmid2  36967  3dim1  38338  3dim2  38339  3dim3  38340  3atlem3  38356  3atlem7  38360  lvolnle3at  38453  2lplnja  38490  paddasslem18  38708  lhpexle3lem  38882  4atex  38947  cdlemd5  39073  cdleme16  39156  cdleme20  39195  cdleme21j  39207  cdleme21  39208  cdleme32snaw  39306  cdleme32fvcl  39311  cdleme32le  39318  cdlemeg46gf  39404  cdleme48gfv  39408  cdleme50trn12  39423  cdlemg6  39494  cdlemg7N  39497  cdlemg38  39586  cdlemg46  39606  dibvalrel  40034  dihlss  40121  dihglblem5aN  40163  dihmeetbN  40174  dihmeetALTN  40198  dihatlat  40205  dihatexv  40209  dvh3dim2  40319  dvh3dim3N  40320  lclkrlem2h  40385  mapdh8d  40654  mapdh8g  40656  hdmap11lem2  40713  lcmineqlem23  40916  aks4d1p3  40943  aks4d1p5  40945  aks4d1p7d1  40947  aks6d1c2p2  40957  metakunt23  41007  metakunt24  41008  metakunt29  41013  metakunt30  41014  metakunt31  41015  dffltz  41376  ttac  41775  pw2f1ocnv  41776  aomclem5  41800  isnumbasgrplem3  41847  iocmbl  41962  oe0suclim  42027  tfsconcatfv  42091  safesnsupfidom1o  42168  safesnsupfilb  42169  r1rankcld  42990  grur1cld  42991  grucollcld  43019  mnuprd  43035  radcnvrat  43073  bccbc  43104  binomcxp  43116  fnchoice  43713  fiiuncl  43752  eliin2f  43793  founiiun0  43888  axccdom  43921  axccd2  43929  fzisoeu  44010  fperiodmul  44014  upbdrech2  44018  fzdifsuc2  44020  uzfissfz  44036  supxrgere  44043  supxrgelem  44047  supxrge  44048  suplesup  44049  infrpge  44061  xrlexaddrp  44062  xralrple2  44064  infxr  44077  infleinflem1  44080  infleinflem2  44081  infleinf  44082  xralrple3  44084  xrralrecnnge  44100  uzublem  44140  supxrmnf2  44143  infxrpnf  44156  infxrpnf2  44173  supminfxr  44174  supminfxr2  44179  pimxrneun  44199  rexanuz2nf  44203  ioondisj2  44206  iccdifprioo  44229  fmul01lt1lem1  44300  fmul01lt1lem2  44301  limciccioolb  44337  lptioo2  44347  lptioo1  44348  limcicciooub  44353  lptre2pt  44356  limcresiooub  44358  limcresioolb  44359  limcleqr  44360  climfveq  44385  climfveqf  44396  limsupubuzlem  44428  limsupubuz  44429  limsupmnfuzlem  44442  limsupre3uzlem  44451  climxrre  44466  limsup10exlem  44488  cnrefiisplem  44545  climxlim2lem  44561  dfxlim2v  44563  xlimliminflimsup  44578  coskpi2  44582  cosknegpi  44585  icccncfext  44603  cncfiooicclem1  44609  cncfiooicc  44610  cncfiooiccre  44611  dvbdfbdioolem2  44645  ioodvbdlimc1lem1  44647  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnxpaek  44658  dvnprodlem1  44662  dvnprodlem3  44664  volioc  44688  itgioocnicc  44693  iblcncfioo  44694  volico  44699  sublevolico  44700  ismbl3  44702  ovolsplit  44704  volioore  44706  voliooico  44708  voliccico  44715  stoweidlem14  44730  stoweidlem26  44742  stoweidlem28  44744  stoweidlem55  44771  stoweid  44779  stirlinglem5  44794  stirlinglem12  44801  dirkerper  44812  dirkertrigeqlem3  44816  dirkertrigeq  44817  dirkercncflem1  44819  dirkercncflem2  44820  dirkercncf  44823  fourierdlem10  44833  fourierdlem12  44835  fourierdlem24  44847  fourierdlem30  44853  fourierdlem31  44854  fourierdlem32  44855  fourierdlem33  44856  fourierdlem34  44857  fourierdlem35  44858  fourierdlem37  44860  fourierdlem40  44863  fourierdlem41  44864  fourierdlem42  44865  fourierdlem43  44866  fourierdlem44  44867  fourierdlem46  44868  fourierdlem48  44870  fourierdlem49  44871  fourierdlem51  44873  fourierdlem54  44876  fourierdlem62  44884  fourierdlem64  44886  fourierdlem65  44887  fourierdlem70  44892  fourierdlem71  44893  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem78  44900  fourierdlem79  44901  fourierdlem80  44902  fourierdlem81  44903  fourierdlem82  44904  fourierdlem92  44914  fourierdlem93  44915  fourierdlem97  44919  fourierdlem101  44923  fourierdlem102  44924  fourierdlem103  44925  fourierdlem104  44926  fourierdlem109  44931  fourierdlem114  44936  sqwvfoura  44944  sqwvfourb  44945  fourierswlem  44946  fouriersw  44947  elaa2lem  44949  etransclem15  44965  etransclem19  44969  etransclem20  44970  etransclem22  44972  etransclem23  44973  etransclem24  44974  etransclem25  44975  etransclem27  44977  etransclem28  44978  etransclem35  44985  etransclem38  44988  qndenserrnbl  45011  ioorrnopn  45021  ioorrnopnxrlem  45022  ioorrnopnxr  45023  prsal  45034  salexct  45050  issalnnd  45061  sge0sn  45095  sge0tsms  45096  sge0cl  45097  sge0f1o  45098  sge0sup  45107  sge0less  45108  sge0pr  45110  sge0prle  45117  sge0le  45123  sge0split  45125  sge0splitmpt  45127  sge0iunmptlemfi  45129  sge0iunmpt  45134  sge0isum  45143  sge0xaddlem1  45149  sge0xadd  45151  sge0gtfsumgt  45159  nnfoctbdjlem  45171  iundjiun  45176  meadjun  45178  ismeannd  45183  voliunsge0lem  45188  meaiuninc3v  45200  caragenfiiuncl  45231  omeiunltfirp  45235  carageniuncl  45239  caragenunicl  45240  isomenndlem  45246  isomennd  45247  hoicvr  45264  ovnssle  45277  ovn0  45282  ovnsubadd  45288  hsphoidmvle2  45301  hoidmvval0b  45306  hoidmv1lelem1  45307  hoidmv1lelem2  45308  hoidmv1le  45310  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvlelem5  45315  hoidmvle  45316  ovnhoilem1  45317  ovnhoi  45319  ovnlecvr2  45326  hspdifhsp  45332  hoidifhspdmvle  45336  hoiqssbl  45341  hspmbllem1  45342  hspmbllem2  45343  hspmbl  45345  hoimbl  45347  volico2  45357  ovolval2lem  45359  ovnsubadd2lem  45361  ovolval4lem1  45365  ovolval4lem2  45366  ovolval5lem1  45368  vonhoire  45388  iunhoiioo  45392  vonioo  45398  vonicc  45401  vonsn  45407  pimrecltpos  45424  incsmflem  45457  smfpimltxr  45463  smfconst  45465  decsmflem  45482  smfpimgtxr  45496  smfrec  45505  smfpimne2  45556  sharhght  45581  rrx2linest  47428  mofsn2  47511  ipolub00  47618