Theorem pm2.61dan 809

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

This theorem is referenced by:  pm2.61ddan  810  pm2.61dda  811  nfsb4t  2504  sbal2  2535  pm2.61danel  3064  ifeq1da  4495  ifeq2da  4496  ifeq12da  4497  ifclda  4499  ifeqda  4500  ifbothda  4502  2if2  4519  somin1  6035  xpcan  6076  fvmpti  6868  fvmptss  6881  funressn  7025  ovima0  7442  oeoa  8404  oeoe  8406  omabs  8455  eceqoveq  8585  domdifsn  8811  pw2f1olem  8832  mapdom1  8894  imafi  8923  marypha1lem  9153  supval2  9175  infdifsn  9376  ttrcltr  9435  ttrclselem1  9444  trpredlem1  9457  carden2b  9709  fidomtri  9735  dfac12lem2  9884  infunsdom1  9953  infunsdom  9954  itunisuc  10159  gchdomtri  10369  fiminre2  11906  xrmax2  12892  xrmin1  12893  ifle  12913  xnn0lem1lt  12960  xmulneg1  12985  xrsupsslem  13023  xrinfmsslem  13024  fzneuz  13319  seqf1olem1  13743  bccmpl  14004  bcval5  14013  bcpasc  14016  bccl  14017  hasheni  14043  hashfn  14071  hashdom  14075  hashdomi  14076  hashge1  14085  hashbc  14146  pfxval0  14370  sumz  15415  sumss  15417  fsumsplitsn  15437  sumsplit  15461  prod1  15635  prodss  15638  fprodsplitsn  15680  fprodle  15687  bitsmod  16124  sadadd2lem2  16138  sadcaddlem  16145  gcddvds  16191  gcdcl  16194  gcdneg  16210  dvdslcm  16284  lcmcl  16287  lcmneg  16289  lcmgcd  16293  lcmfcl  16314  dvdslcmf  16317  pcgcd  16560  pcmpt  16574  pcmpt2  16575  pcprod  16577  fldivp1  16579  prmreclem4  16601  vdwlem6  16668  ramub1lem1  16708  cidpropd  17400  rescabs  17528  rescabsOLD  17529  lubval  18055  glbval  18068  joinval  18076  meetval  18090  acsexdimd  18258  gsumpropd2lem  18344  gsumval2  18351  mulgfval  18683  f1otrspeq  19036  pmtrfinv  19050  psgnunilem1  19082  gsumval3  19489  ablfac1c  19655  ablfac1eu  19657  mgpress  19716  mgpressOLD  19717  frlmsslsp  20984  psrbas  21128  resspsrbas  21165  mplmonmul  21218  mplcoe1  21219  mplcoe5  21222  opsrle  21229  opsrbaslem  21231  opsrbaslemOLD  21232  psrbaspropd  21387  mplbaspropd  21389  mdetdiag  21729  mdetunilem7  21748  mdetunilem9  21750  maducoeval2  21770  madurid  21774  opnnei  22252  restbas  22290  hauspwdom  22633  ptcmplem5  23188  xrsmopn  23956  xrhmeo  24090  lebnum  24108  pcoass  24168  pcorevlem  24170  icombl  24709  ioombl  24710  mbfconstlem  24772  mbfima  24775  i1fd  24826  mbfi1fseqlem5  24865  itg2const2  24887  itg2seq  24888  itg2uba  24889  itg2splitlem  24894  itg2split  24895  itg2monolem1  24896  itg2gt0  24906  itg2cnlem1  24907  itg2cnlem2  24908  iblss  24950  iblss2  24951  itgss  24957  bddmulibl  24984  coemullem  25392  aaliou2b  25482  isppw2  26245  mule1  26278  ppip1le  26291  dchrelbas3  26367  dchrpt  26396  bposlem3  26415  bposlem5  26417  bposlem6  26418  lgslem4  26429  lgsneg  26450  lgsmod  26452  lgsdilem  26453  lgsdir  26461  lgsdi  26463  lgsne0  26464  lgsquad3  26516  dchrvmasum2if  26626  midexlem  27034  colperpex  27075  outpasch  27097  hlpasch  27098  lnopp2hpgb  27105  lmieu  27126  inaghl  27187  cgrg3col4  27195  pthdlem1  28113  nmcfnlbi  30393  elpreq  30857  disjdifprg  30893  disjun0  30913  f1ocnt  31102  xrge0npcan  31282  psgnfzto1stlem  31346  cyc3genpmlem  31397  cyc3conja  31403  archiabl  31431  orngsqr  31482  1smat1  31733  esumcst  32010  esumrnmpt2  32015  hasheuni  32032  esumcvg  32033  ddemeas  32183  omssubadd  32246  eulerpartlemgc  32308  eulerpartlemb  32314  plymulx  32506  signswmnd  32515  pthhashvtx  33068  erdsze2lem1  33144  mrsubvrs  33463  unblimceq0lem  34665  unbdqndv2lem2  34669  knoppndvlem10  34680  wl-spae  35659  wl-cbvalnaed  35670  wl-nfeqfb  35674  unccur  35739  poimirlem15  35771  poimirlem22  35778  itg2addnclem  35807  itg2addnclem2  35808  iblmulc2nc  35821  ftc1anclem5  35833  ftc1anc  35837  dvasin  35840  areacirclem5  35848  exmid2  36236  3dim1  37460  3dim2  37461  3dim3  37462  3atlem3  37478  3atlem7  37482  lvolnle3at  37575  2lplnja  37612  paddasslem18  37830  lhpexle3lem  38004  4atex  38069  cdlemd5  38195  cdleme16  38278  cdleme20  38317  cdleme21j  38329  cdleme21  38330  cdleme32snaw  38428  cdleme32fvcl  38433  cdleme32le  38440  cdlemeg46gf  38526  cdleme48gfv  38530  cdleme50trn12  38545  cdlemg6  38616  cdlemg7N  38619  cdlemg38  38708  cdlemg46  38728  dibvalrel  39156  dihlss  39243  dihglblem5aN  39285  dihmeetbN  39296  dihmeetALTN  39320  dihatlat  39327  dihatexv  39331  dvh3dim2  39441  dvh3dim3N  39442  lclkrlem2h  39507  mapdh8d  39776  mapdh8g  39778  hdmap11lem2  39835  lcmineqlem23  40039  aks4d1p3  40066  aks4d1p5  40068  aks4d1p7d1  40070  metakunt23  40127  metakunt24  40128  metakunt29  40133  metakunt30  40134  metakunt31  40135  dffltz  40451  ttac  40838  pw2f1ocnv  40839  aomclem5  40863  isnumbasgrplem3  40910  iocmbl  41024  r1rankcld  41802  grur1cld  41803  grucollcld  41831  mnuprd  41847  radcnvrat  41885  bccbc  41916  binomcxp  41928  fnchoice  42525  fiiuncl  42566  eliin2f  42607  founiiun0  42681  axccdom  42715  axccd2  42722  fzisoeu  42793  fperiodmul  42797  upbdrech2  42801  fzdifsuc2  42803  uzfissfz  42819  supxrgere  42826  supxrgelem  42830  supxrge  42831  suplesup  42832  infrpge  42844  xrlexaddrp  42845  xralrple2  42847  infxr  42860  infleinflem1  42863  infleinflem2  42864  infleinf  42865  xralrple3  42867  xrralrecnnge  42884  uzublem  42924  supxrmnf2  42927  infxrpnf  42940  infxrpnf2  42957  supminfxr  42958  supminfxr2  42963  ioondisj2  42985  iccdifprioo  43008  fmul01lt1lem1  43079  fmul01lt1lem2  43080  limciccioolb  43116  lptioo2  43126  lptioo1  43127  limcicciooub  43132  lptre2pt  43135  limcresiooub  43137  limcresioolb  43138  limcleqr  43139  climfveq  43164  climfveqf  43175  limsupubuzlem  43207  limsupubuz  43208  limsupmnfuzlem  43221  limsupre3uzlem  43230  climxrre  43245  limsup10exlem  43267  cnrefiisplem  43324  climxlim2lem  43340  dfxlim2v  43342  xlimliminflimsup  43357  coskpi2  43361  cosknegpi  43364  icccncfext  43382  cncfiooicclem1  43388  cncfiooicc  43389  cncfiooiccre  43390  dvbdfbdioolem2  43424  ioodvbdlimc1lem1  43426  ioodvbdlimc1lem2  43427  ioodvbdlimc2lem  43429  dvnxpaek  43437  dvnprodlem1  43441  dvnprodlem3  43443  volioc  43467  itgioocnicc  43472  iblcncfioo  43473  volico  43478  sublevolico  43479  ismbl3  43481  ovolsplit  43483  volioore  43485  voliooico  43487  voliccico  43494  stoweidlem14  43509  stoweidlem26  43521  stoweidlem28  43523  stoweidlem55  43550  stoweid  43558  stirlinglem5  43573  stirlinglem12  43580  dirkerper  43591  dirkertrigeqlem3  43595  dirkertrigeq  43596  dirkercncflem1  43598  dirkercncflem2  43599  dirkercncf  43602  fourierdlem10  43612  fourierdlem12  43614  fourierdlem24  43626  fourierdlem30  43632  fourierdlem31  43633  fourierdlem32  43634  fourierdlem33  43635  fourierdlem34  43636  fourierdlem35  43637  fourierdlem37  43639  fourierdlem40  43642  fourierdlem41  43643  fourierdlem42  43644  fourierdlem43  43645  fourierdlem44  43646  fourierdlem46  43647  fourierdlem48  43649  fourierdlem49  43650  fourierdlem51  43652  fourierdlem54  43655  fourierdlem62  43663  fourierdlem64  43665  fourierdlem65  43666  fourierdlem70  43671  fourierdlem71  43672  fourierdlem73  43674  fourierdlem74  43675  fourierdlem75  43676  fourierdlem78  43679  fourierdlem79  43680  fourierdlem80  43681  fourierdlem81  43682  fourierdlem82  43683  fourierdlem92  43693  fourierdlem93  43694  fourierdlem97  43698  fourierdlem101  43702  fourierdlem102  43703  fourierdlem103  43704  fourierdlem104  43705  fourierdlem109  43710  fourierdlem114  43715  sqwvfoura  43723  sqwvfourb  43724  fourierswlem  43725  fouriersw  43726  elaa2lem  43728  etransclem15  43744  etransclem19  43748  etransclem20  43749  etransclem22  43751  etransclem23  43752  etransclem24  43753  etransclem25  43754  etransclem27  43756  etransclem28  43757  etransclem35  43764  etransclem38  43767  qndenserrnbl  43790  ioorrnopn  43800  ioorrnopnxrlem  43801  ioorrnopnxr  43802  prsal  43813  salexct  43827  issalnnd  43838  sge0sn  43871  sge0tsms  43872  sge0cl  43873  sge0f1o  43874  sge0sup  43883  sge0less  43884  sge0pr  43886  sge0prle  43893  sge0le  43899  sge0split  43901  sge0splitmpt  43903  sge0iunmptlemfi  43905  sge0iunmpt  43910  sge0isum  43919  sge0xaddlem1  43925  sge0xadd  43927  sge0gtfsumgt  43935  nnfoctbdjlem  43947  iundjiun  43952  meadjun  43954  ismeannd  43959  voliunsge0lem  43964  meaiuninc3v  43976  caragenfiiuncl  44007  omeiunltfirp  44011  carageniuncl  44015  caragenunicl  44016  isomenndlem  44022  isomennd  44023  hoicvr  44040  ovnssle  44053  ovn0  44058  ovnsubadd  44064  hsphoidmvle2  44077  hoidmvval0b  44082  hoidmv1lelem1  44083  hoidmv1lelem2  44084  hoidmv1le  44086  hoidmvlelem2  44088  hoidmvlelem3  44089  hoidmvlelem5  44091  hoidmvle  44092  ovnhoilem1  44093  ovnhoi  44095  ovnlecvr2  44102  hspdifhsp  44108  hoidifhspdmvle  44112  hoiqssbl  44117  hspmbllem1  44118  hspmbllem2  44119  hspmbl  44121  hoimbl  44123  volico2  44133  ovolval2lem  44135  ovnsubadd2lem  44137  ovolval4lem1  44141  ovolval4lem2  44142  ovolval5lem1  44144  vonhoire  44164  iunhoiioo  44168  vonioo  44174  vonicc  44177  vonsn  44183  pimrecltpos  44197  incsmflem  44228  smfpimltxr  44234  smfconst  44236  decsmflem  44252  smfpimgtxr  44266  smfrec  44274  sharhght  44332  rrx2linest  46040  mofsn2  46124  ipolub00  46231