Theorem pm2.61dan 824

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

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

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 210  df-an 401

This theorem is referenced by:  pm2.61ddan  825  pm2.61dda  826  nfsb4t  2533  sbal2  2563  pm2.61danel  3078  ifeq1da  4515  ifeq2da  4516  ifeq12da  4517  ifclda  4519  ifeqda  4520  ifbothda  4522  2if2  4539  somin1  6124  xpcan  6166  fvmpti  6978  fvmptss  6992  funressn  7146  ovima0  7579  ordsuci  7795  suppssov1  8181  suppssov2  8182  oeoa  8571  oeoe  8573  omabs  8625  eceqoveq  8808  domdifsn  9036  pw2f1olem  9057  mapdom1  9118  marypha1lem  9381  supval2  9403  infdifsn  9614  ttrcltr  9673  ttrclselem1  9682  carden2b  9941  fidomtri  9967  dfac12lem2  10116  infunsdom1  10183  infunsdom  10184  itunisuc  10391  gchdomtri  10602  fiminre2  12154  xrmax2  13193  xrmin1  13194  ifle  13214  xnn0lem1lt  13261  xmulneg1  13286  xrsupsslem  13324  xrinfmsslem  13325  fzneuz  13627  seqf1olem1  14068  bccmpl  14336  bcval5  14345  bcpasc  14348  bccl  14349  hasheni  14375  hashfn  14402  hashdom  14406  hashdomi  14407  hashge1  14416  hashbc  14480  pfxval0  14704  sumz  15763  sumss  15765  fsumsplitsn  15785  sumsplit  15809  prod1  15988  prodss  15991  fprodsplitsn  16033  fprodle  16040  bitsmod  16484  sadadd2lem2  16498  sadcaddlem  16505  gcddvds  16551  gcdcl  16554  gcdneg  16570  dvdslcm  16646  lcmcl  16649  lcmneg  16651  lcmgcd  16655  lcmfcl  16676  dvdslcmf  16679  pcgcd  16928  pcmpt  16942  pcmpt2  16943  pcprod  16945  fldivp1  16947  prmreclem4  16969  vdwlem6  17036  ramub1lem1  17076  cidpropd  17756  rescabs  17880  lubval  18400  glbval  18413  joinval  18421  meetval  18435  acsexdimd  18605  gsumpropd2lem  18727  gsumval2  18734  mulgfval  19126  f1otrspeq  19508  pmtrfinv  19522  psgnunilem1  19554  gsumval3  19968  ablfac1c  20134  ablfac1eu  20136  mgpress  20217  orngsqr  20938  frlmsslsp  21906  psrbas  22044  resspsrbas  22083  mplmonmul  22147  mplcoe1  22148  mplcoe5  22151  opsrle  22158  opsrbaslem  22160  psrbaspropd  22354  mplbaspropd  22356  mdetdiag  22717  mdetunilem7  22736  mdetunilem9  22738  maducoeval2  22758  madurid  22762  opnnei  23238  restbas  23276  hauspwdom  23619  ptcmplem5  24174  xrsmopn  24931  xrhmeo  25066  lebnum  25084  pcoass  25144  pcorevlem  25146  icombl  25684  ioombl  25685  mbfconstlem  25747  mbfima  25750  i1fd  25801  mbfi1fseqlem5  25839  itg2const2  25861  itg2seq  25862  itg2uba  25863  itg2splitlem  25868  itg2split  25869  itg2monolem1  25870  itg2gt0  25880  itg2cnlem1  25881  itg2cnlem2  25882  iblss  25925  iblss2  25926  itgss  25932  bddmulibl  25959  coemullem  26368  plymulidp  26404  aaliou2b  26463  isppw2  27237  mule1  27270  ppip1le  27283  dchrelbas3  27360  dchrpt  27389  bposlem3  27408  bposlem5  27410  bposlem6  27411  lgslem4  27422  lgsneg  27443  lgsmod  27445  lgsdilem  27446  lgsdir  27454  lgsdi  27456  lgsne0  27457  lgsquad3  27509  dchrvmasum2if  27619  maxs2  27892  mins1  27893  z12bday  28636  tglnpt4  28882  midexlem  28923  colperpex  28964  outpasch  28986  hlpasch  28987  lnopp2hpgb  28994  lmieu  29036  inaghl  29097  cgrg3col4  29105  pthdlem1  30024  nmcfnlbi  32313  elpreq  32784  prssad  32785  prssbd  32786  disjdifprg  32830  disjun0  32850  argcj  33005  f1ocnt  33057  xrge0npcan  33253  psgnfzto1stlem  33333  cyc3genpmlem  33384  cyc3conja  33390  archiabl  33431  erlval  33491  1arithufdlem3  33753  1arithufd  33755  psrmonmul  33857  esplyfval3  33879  resssra  33894  lbslelsp  33905  constrrecl  34076  constrinvcl  34080  constrsqrtcl  34086  1smat1  34111  esumcst  34370  esumrnmpt2  34375  hasheuni  34392  esumcvg  34393  ddemeas  34543  omssubadd  34607  eulerpartlemgc  34669  eulerpartlemb  34675  signswmnd  34861  fineqvnttrclselem1  35429  pthhashvtx  35491  erdsze2lem1  35566  mrsubvrs  35885  unblimceq0lem  36957  unbdqndv2lem2  36961  knoppndvlem10  36972  wl-spae  38036  wl-cbvalnaed  38047  wl-nfeqfb  38051  unccur  38114  poimirlem15  38146  poimirlem22  38153  itg2addnclem  38182  itg2addnclem2  38183  iblmulc2nc  38196  ftc1anclem5  38208  ftc1anc  38212  dvasin  38215  areacirclem5  38223  exmid2  38610  3dim1  40103  3dim2  40104  3dim3  40105  3atlem3  40121  3atlem7  40125  lvolnle3at  40218  2lplnja  40255  paddasslem18  40473  lhpexle3lem  40647  4atex  40712  cdlemd5  40838  cdleme16  40921  cdleme20  40960  cdleme21j  40972  cdleme21  40973  cdleme32snaw  41071  cdleme32fvcl  41076  cdleme32le  41083  cdlemeg46gf  41169  cdleme48gfv  41173  cdleme50trn12  41188  cdlemg6  41259  cdlemg7N  41262  cdlemg38  41351  cdlemg46  41371  dibvalrel  41799  dihlss  41886  dihglblem5aN  41928  dihmeetbN  41939  dihmeetALTN  41963  dihatlat  41970  dihatexv  41974  dvh3dim2  42084  dvh3dim3N  42085  lclkrlem2h  42150  mapdh8d  42419  mapdh8g  42421  hdmap11lem2  42478  lcmineqlem23  42680  aks4d1p3  42707  aks4d1p5  42709  aks4d1p7d1  42711  posbezout  42729  aks6d1c2p2  42748  aks6d1c4  42753  aks6d1c5lem1  42765  aks6d1c6lem3  42801  aks6d1c6lem4  42802  bcled  42807  bcle2d  42808  aks6d1c7  42813  grpods  42823  unitscyglem2  42825  unitscyglem4  42827  aks5lem8  42830  dffltz  43228  ttac  43625  pw2f1ocnv  43626  aomclem5  43647  isnumbasgrplem3  43694  iocmbl  43802  oe0suclim  43866  tfsconcatfv  43930  safesnsupfidom1o  44005  safesnsupfilb  44006  r1rankcld  44819  grur1cld  44820  grucollcld  44834  mnuprd  44850  radcnvrat  44888  bccbc  44919  binomcxp  44931  fnchoice  45607  fiiuncl  45643  eliin2f  45680  founiiun0  45766  axccdom  45796  axccd2  45803  fzisoeu  45877  fperiodmul  45881  upbdrech2  45885  fzdifsuc2  45887  uzfissfz  45900  supxrgere  45907  supxrgelem  45911  supxrge  45912  suplesup  45913  infrpge  45925  xrlexaddrp  45926  xralrple2  45928  infxr  45940  infleinflem1  45943  infleinflem2  45944  infleinf  45945  xralrple3  45947  xrralrecnnge  45963  uzublem  46002  supxrmnf2  46005  infxrpnf  46018  infxrpnf2  46035  supminfxr  46036  supminfxr2  46041  pimxrneun  46060  rexanuz2nf  46064  ioondisj2  46067  iccdifprioo  46090  fmul01lt1lem1  46158  fmul01lt1lem2  46159  limciccioolb  46195  lptioo2  46205  lptioo1  46206  limcicciooub  46209  lptre2pt  46212  limcresiooub  46214  limcresioolb  46215  limcleqr  46216  climfveq  46241  climfveqf  46252  limsupubuzlem  46284  limsupubuz  46285  limsupmnfuzlem  46298  limsupre3uzlem  46307  climxrre  46322  limsup10exlem  46344  cnrefiisplem  46401  climxlim2lem  46417  dfxlim2v  46419  xlimliminflimsup  46434  coskpi2  46438  cosknegpi  46441  icccncfext  46459  cncfiooicclem1  46465  cncfiooicc  46466  cncfiooiccre  46467  dvbdfbdioolem2  46501  ioodvbdlimc1lem1  46503  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  dvnxpaek  46514  dvnprodlem1  46518  dvnprodlem3  46520  volioc  46544  itgioocnicc  46549  iblcncfioo  46550  volico  46555  sublevolico  46556  ismbl3  46558  ovolsplit  46560  volioore  46562  voliooico  46564  voliccico  46571  stoweidlem14  46586  stoweidlem26  46598  stoweidlem28  46600  stoweidlem55  46627  stoweid  46635  stirlinglem5  46650  stirlinglem12  46657  dirkerper  46668  dirkertrigeqlem3  46672  dirkertrigeq  46673  dirkercncflem1  46675  dirkercncflem2  46676  dirkercncf  46679  fourierdlem10  46689  fourierdlem12  46691  fourierdlem24  46703  fourierdlem30  46709  fourierdlem31  46710  fourierdlem32  46711  fourierdlem33  46712  fourierdlem34  46713  fourierdlem35  46714  fourierdlem37  46716  fourierdlem40  46719  fourierdlem41  46720  fourierdlem42  46721  fourierdlem43  46722  fourierdlem44  46723  fourierdlem46  46724  fourierdlem48  46726  fourierdlem49  46727  fourierdlem51  46729  fourierdlem54  46732  fourierdlem62  46740  fourierdlem64  46742  fourierdlem65  46743  fourierdlem70  46748  fourierdlem71  46749  fourierdlem73  46751  fourierdlem74  46752  fourierdlem75  46753  fourierdlem78  46756  fourierdlem79  46757  fourierdlem80  46758  fourierdlem81  46759  fourierdlem82  46760  fourierdlem92  46770  fourierdlem93  46771  fourierdlem97  46775  fourierdlem101  46779  fourierdlem102  46780  fourierdlem103  46781  fourierdlem104  46782  fourierdlem109  46787  fourierdlem114  46792  sqwvfoura  46800  sqwvfourb  46801  fourierswlem  46802  fouriersw  46803  elaa2lem  46805  etransclem15  46821  etransclem19  46825  etransclem20  46826  etransclem22  46828  etransclem23  46829  etransclem24  46830  etransclem25  46831  etransclem27  46833  etransclem28  46834  etransclem35  46841  etransclem38  46844  qndenserrnbl  46867  ioorrnopn  46877  ioorrnopnxrlem  46878  ioorrnopnxr  46879  prsal  46890  salexct  46906  issalnnd  46917  sge0sn  46951  sge0tsms  46952  sge0cl  46953  sge0f1o  46954  sge0sup  46963  sge0less  46964  sge0pr  46966  sge0prle  46973  sge0le  46979  sge0split  46981  sge0splitmpt  46983  sge0iunmptlemfi  46985  sge0iunmpt  46990  sge0isum  46999  sge0xaddlem1  47005  sge0xadd  47007  sge0gtfsumgt  47015  nnfoctbdjlem  47027  iundjiun  47032  meadjun  47034  ismeannd  47039  voliunsge0lem  47044  meaiuninc3v  47056  caragenfiiuncl  47087  omeiunltfirp  47091  carageniuncl  47095  caragenunicl  47096  isomenndlem  47102  isomennd  47103  hoicvr  47120  ovnssle  47133  ovn0  47138  ovnsubadd  47144  hsphoidmvle2  47157  hoidmvval0b  47162  hoidmv1lelem1  47163  hoidmv1lelem2  47164  hoidmv1le  47166  hoidmvlelem2  47168  hoidmvlelem3  47169  hoidmvlelem5  47171  hoidmvle  47172  ovnhoilem1  47173  ovnhoi  47175  ovnlecvr2  47182  hspdifhsp  47188  hoidifhspdmvle  47192  hoiqssbl  47197  hspmbllem1  47198  hspmbllem2  47199  hspmbl  47201  hoimbl  47203  volico2  47213  ovolval2lem  47215  ovnsubadd2lem  47217  ovolval4lem1  47221  ovolval4lem2  47222  ovolval5lem1  47224  vonhoire  47244  iunhoiioo  47248  vonioo  47254  vonicc  47257  vonsn  47263  pimrecltpos  47280  incsmflem  47313  smfpimltxr  47319  smfconst  47321  decsmflem  47338  smfpimgtxr  47352  smfrec  47361  smfpimne2  47412  sharhght  47437  rrx2linest  49373  mofsn2  49474  ipolub00  49622  resccat  49703  initopropdlemlem  49868  prcof1  50017