Theorem pm2.61dan 811

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

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

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 209  df-an 399

This theorem is referenced by:  pm2.61ddan  812  pm2.61dda  813  nfsb4t  2539  sbal2  2573  sbal2OLD  2574  nfsb4tALT  2604  pm2.61danel  3137  ifeq1da  4497  ifeq2da  4498  ifeq12da  4499  ifclda  4501  ifeqda  4502  ifbothda  4504  2if2  4520  somin1  5993  xpcan  6033  fvmpti  6767  fvmptss  6780  funressn  6921  ovima0  7327  oeoa  8223  oeoe  8225  omabs  8274  eceqoveq  8402  domdifsn  8600  pw2f1olem  8621  mapdom1  8682  marypha1lem  8897  supval2  8919  infdifsn  9120  carden2b  9396  fidomtri  9422  dfac12lem2  9570  infunsdom1  9635  infunsdom  9636  itunisuc  9841  gchdomtri  10051  xrmax2  12570  xrmin1  12571  ifle  12591  xnn0lem1lt  12638  xmulneg1  12663  xrsupsslem  12701  xrinfmsslem  12702  fzneuz  12989  seqf1olem1  13410  bccmpl  13670  bcval5  13679  bcpasc  13682  bccl  13683  hasheni  13709  hashfn  13737  hashdom  13741  hashdomi  13742  hashge1  13751  hashbc  13812  pfxval0  14038  sumz  15079  sumss  15081  fsumsplitsn  15100  sumsplit  15123  prod1  15298  prodss  15301  fprodsplitsn  15343  fprodle  15350  bitsmod  15785  sadadd2lem2  15799  sadcaddlem  15806  gcddvds  15852  gcdcl  15855  gcdneg  15870  dvdslcm  15942  lcmcl  15945  lcmneg  15947  lcmgcd  15951  lcmfcl  15972  dvdslcmf  15975  pcgcd  16214  pcmpt  16228  pcmpt2  16229  pcprod  16231  fldivp1  16233  prmreclem4  16255  vdwlem6  16322  ramub1lem1  16362  cidpropd  16980  rescabs  17103  lubval  17594  glbval  17607  joinval  17615  meetval  17629  acsexdimd  17793  gsumpropd2lem  17889  gsumval2  17896  mulgfval  18226  f1otrspeq  18575  pmtrfinv  18589  psgnunilem1  18621  gsumval3  19027  ablfac1c  19193  ablfac1eu  19195  mgpress  19250  psrbas  20158  resspsrbas  20195  mplmonmul  20245  mplcoe1  20246  mplcoe5  20249  opsrle  20256  opsrbaslem  20258  psrbaspropd  20403  mplbaspropd  20405  frlmsslsp  20940  mdetdiag  21208  mdetunilem7  21227  mdetunilem9  21229  maducoeval2  21249  madurid  21253  opnnei  21728  restbas  21766  hauspwdom  22109  ptcmplem5  22664  xrsmopn  23420  xrhmeo  23550  lebnum  23568  pcoass  23628  pcorevlem  23630  icombl  24165  ioombl  24166  mbfconstlem  24228  mbfima  24231  i1fd  24282  mbfi1fseqlem5  24320  itg2const2  24342  itg2seq  24343  itg2uba  24344  itg2splitlem  24349  itg2split  24350  itg2monolem1  24351  itg2gt0  24361  itg2cnlem1  24362  itg2cnlem2  24363  iblss  24405  iblss2  24406  itgss  24412  bddmulibl  24439  coemullem  24840  aaliou2b  24930  isppw2  25692  mule1  25725  ppip1le  25738  dchrelbas3  25814  dchrpt  25843  bposlem3  25862  bposlem5  25864  bposlem6  25865  lgslem4  25876  lgsneg  25897  lgsmod  25899  lgsdilem  25900  lgsdir  25908  lgsdi  25910  lgsne0  25911  lgsquad3  25963  dchrvmasum2if  26073  midexlem  26478  colperpex  26519  outpasch  26541  hlpasch  26542  lnopp2hpgb  26549  lmieu  26570  inaghl  26631  cgrg3col4  26639  pthdlem1  27547  nmcfnlbi  29829  elpreq  30290  disjdifprg  30325  disjun0  30345  f1ocnt  30525  xrge0npcan  30681  psgnfzto1stlem  30742  cyc3genpmlem  30793  cyc3conja  30799  archiabl  30827  orngsqr  30877  1smat1  31069  esumcst  31322  esumrnmpt2  31327  hasheuni  31344  esumcvg  31345  ddemeas  31495  omssubadd  31558  eulerpartlemgc  31620  eulerpartlemb  31626  plymulx  31818  signswmnd  31827  pthhashvtx  32374  erdsze2lem1  32450  mrsubvrs  32769  trpredlem1  33066  unblimceq0lem  33845  unbdqndv2lem2  33849  knoppndvlem10  33860  wl-spae  34776  wl-cbvalnaed  34787  wl-nfeqfb  34791  unccur  34890  poimirlem15  34922  poimirlem22  34929  itg2addnclem  34958  itg2addnclem2  34959  iblmulc2nc  34972  ftc1anclem5  34986  ftc1anc  34990  dvasin  34993  areacirclem5  35001  exmid2  35392  3dim1  36618  3dim2  36619  3dim3  36620  3atlem3  36636  3atlem7  36640  lvolnle3at  36733  2lplnja  36770  paddasslem18  36988  lhpexle3lem  37162  4atex  37227  cdlemd5  37353  cdleme16  37436  cdleme20  37475  cdleme21j  37487  cdleme21  37488  cdleme32snaw  37586  cdleme32fvcl  37591  cdleme32le  37598  cdlemeg46gf  37684  cdleme48gfv  37688  cdleme50trn12  37703  cdlemg6  37774  cdlemg7N  37777  cdlemg38  37866  cdlemg46  37886  dibvalrel  38314  dihlss  38401  dihglblem5aN  38443  dihmeetbN  38454  dihmeetALTN  38478  dihatlat  38485  dihatexv  38489  dvh3dim2  38599  dvh3dim3N  38600  lclkrlem2h  38665  mapdh8d  38934  mapdh8g  38936  hdmap11lem2  38993  dffltz  39320  ttac  39682  pw2f1ocnv  39683  aomclem5  39707  isnumbasgrplem3  39754  iocmbl  39868  r1rankcld  40616  grur1cld  40617  grucollcld  40645  mnuprd  40661  radcnvrat  40695  bccbc  40726  binomcxp  40738  fnchoice  41335  fiiuncl  41376  eliin2f  41419  founiiun0  41500  axccdom  41536  axccd2  41545  fzisoeu  41616  fperiodmul  41620  upbdrech2  41624  fzdifsuc2  41626  uzfissfz  41643  supxrgere  41650  supxrgelem  41654  supxrge  41655  suplesup  41656  infrpge  41668  xrlexaddrp  41669  xralrple2  41671  infxr  41684  infleinflem1  41687  infleinflem2  41688  infleinf  41689  xralrple3  41691  fiminre2  41695  xrralrecnnge  41711  uzublem  41753  supxrmnf2  41756  infxrpnf  41770  infxrpnf2  41788  supminfxr  41789  supminfxr2  41794  ioondisj2  41816  iccdifprioo  41841  fmul01lt1lem1  41914  fmul01lt1lem2  41915  limciccioolb  41951  lptioo2  41961  lptioo1  41962  limcicciooub  41967  lptre2pt  41970  limcresiooub  41972  limcresioolb  41973  limcleqr  41974  climfveq  41999  climfveqf  42010  limsupubuzlem  42042  limsupubuz  42043  limsupmnfuzlem  42056  limsupre3uzlem  42065  climxrre  42080  limsup10exlem  42102  cnrefiisplem  42159  climxlim2lem  42175  dfxlim2v  42177  xlimliminflimsup  42192  coskpi2  42196  cosknegpi  42199  icccncfext  42219  cncfiooicclem1  42225  cncfiooicc  42226  cncfiooiccre  42227  dvbdfbdioolem2  42263  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnxpaek  42276  dvnprodlem1  42280  dvnprodlem3  42282  volioc  42306  itgioocnicc  42311  iblcncfioo  42312  volico  42317  sublevolico  42318  ismbl3  42320  ovolsplit  42322  volioore  42324  voliooico  42326  voliccico  42333  stoweidlem14  42348  stoweidlem26  42360  stoweidlem28  42362  stoweidlem55  42389  stoweid  42397  stirlinglem5  42412  stirlinglem12  42419  dirkerper  42430  dirkertrigeqlem3  42434  dirkertrigeq  42435  dirkercncflem1  42437  dirkercncflem2  42438  dirkercncf  42441  fourierdlem10  42451  fourierdlem12  42453  fourierdlem24  42465  fourierdlem30  42471  fourierdlem31  42472  fourierdlem32  42473  fourierdlem33  42474  fourierdlem34  42475  fourierdlem35  42476  fourierdlem37  42478  fourierdlem40  42481  fourierdlem41  42482  fourierdlem42  42483  fourierdlem43  42484  fourierdlem44  42485  fourierdlem46  42486  fourierdlem48  42488  fourierdlem49  42489  fourierdlem51  42491  fourierdlem54  42494  fourierdlem62  42502  fourierdlem64  42504  fourierdlem65  42505  fourierdlem70  42510  fourierdlem71  42511  fourierdlem73  42513  fourierdlem74  42514  fourierdlem75  42515  fourierdlem78  42518  fourierdlem79  42519  fourierdlem80  42520  fourierdlem81  42521  fourierdlem82  42522  fourierdlem92  42532  fourierdlem93  42533  fourierdlem97  42537  fourierdlem101  42541  fourierdlem102  42542  fourierdlem103  42543  fourierdlem104  42544  fourierdlem109  42549  fourierdlem114  42554  sqwvfoura  42562  sqwvfourb  42563  fourierswlem  42564  fouriersw  42565  elaa2lem  42567  etransclem15  42583  etransclem19  42587  etransclem20  42588  etransclem22  42590  etransclem23  42591  etransclem24  42592  etransclem25  42593  etransclem27  42595  etransclem28  42596  etransclem35  42603  etransclem38  42606  qndenserrnbl  42629  ioorrnopn  42639  ioorrnopnxrlem  42640  ioorrnopnxr  42641  prsal  42652  salexct  42666  issalnnd  42677  sge0sn  42710  sge0tsms  42711  sge0cl  42712  sge0f1o  42713  sge0sup  42722  sge0less  42723  sge0pr  42725  sge0prle  42732  sge0le  42738  sge0split  42740  sge0splitmpt  42742  sge0iunmptlemfi  42744  sge0iunmpt  42749  sge0isum  42758  sge0xaddlem1  42764  sge0xadd  42766  sge0gtfsumgt  42774  nnfoctbdjlem  42786  iundjiun  42791  meadjun  42793  ismeannd  42798  voliunsge0lem  42803  meaiuninc3v  42815  caragenfiiuncl  42846  omeiunltfirp  42850  carageniuncl  42854  caragenunicl  42855  isomenndlem  42861  isomennd  42862  hoicvr  42879  ovnssle  42892  ovn0  42897  ovnsubadd  42903  hsphoidmvle2  42916  hoidmvval0b  42921  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1le  42925  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvlelem5  42930  hoidmvle  42931  ovnhoilem1  42932  ovnhoi  42934  ovnlecvr2  42941  hspdifhsp  42947  hoidifhspdmvle  42951  hoiqssbl  42956  hspmbllem1  42957  hspmbllem2  42958  hspmbl  42960  hoimbl  42962  volico2  42972  ovolval2lem  42974  ovnsubadd2lem  42976  ovolval4lem1  42980  ovolval4lem2  42981  ovolval5lem1  42983  vonhoire  43003  iunhoiioo  43007  vonioo  43013  vonicc  43016  vonsn  43022  pimrecltpos  43036  incsmflem  43067  smfpimltxr  43073  smfconst  43075  decsmflem  43091  smfpimgtxr  43105  smfrec  43113  sharhght  43171  ichnfimlem3  43672  rrx2linest  44778