Theorem simp3d 1145

Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
3simp1d.1	⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp3d	⊢ (𝜑 → 𝜃)

Proof of Theorem simp3d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp3 1139	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1087

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  df-3an 1089

This theorem is referenced by:  simp3bi  1148  f1dom3fv3dif  7214  f1dom3el3dif  7215  oeeui  8529  resixp  8872  domssex2  9066  cantnflem1c  9597  cantnflem1  9599  cantnflem3  9601  cantnflem4  9602  fpwwe2lem6  10548  canthnumlem  10560  canthp1lem2  10565  wununi  10618  wunpw  10619  wunpr  10621  lelttrdi  11297  ixxdisj  13302  ixxun  13303  ixxss1  13305  ixxss2  13306  ixxss12  13307  ixxub  13308  ixxlb  13309  lbioo  13318  elicore  13340  iccsupr  13384  icodisj  13418  xov1plusxeqvd  13440  intfracq  13807  fldiv  13808  seqf1olem2  13993  cjmul  15093  icco1  15491  sumtp  15700  rpnnen2lem10  16179  ruclem2  16188  ruclem3  16189  ruclem9  16194  ruclem12  16197  dvdslegcd  16462  prmdvdsbc  16685  crth  16737  eulerthlem1  16740  eulerthlem2  16741  pcpremul  16803  prmreclem2  16877  prmreclem3  16878  4sqlem13  16917  sectcan  17711  sectco  17712  sectmon  17738  monsect  17739  funcid  17826  funcco  17827  funcsect  17828  invfuc  17933  fuciso  17934  coapm  18027  catciso  18067  postr  18275  ipodrsima  18496  psref2  18525  psasym  18531  mhm0  18751  submcl  18769  submmnd  18770  eqger  19142  eqgcpbl  19146  ghmqusnsglem1  19244  ghmquskerlem1  19247  gaorber  19272  orbsta  19277  cayleyth  19379  pmtrrn2  19424  pmtrfinv  19425  pmtrfmvdn0  19426  dfod2  19528  sylow2blem1  19584  sylow2blem3  19586  dprdcntz  19974  dprddisj  19975  dprdffsupp  19980  dpjdisj  20019  ablfac1a  20035  ablfac1b  20036  lmodvsdir  20870  lmhmlin  21020  lbsind  21065  2idlcpblrng  21259  evlsval3  22076  mpfind  22102  mdetunilem2  22587  mdetunilem5  22590  mdetunilem6  22591  mnfnei  23195  cnprcl  23219  lmcvg  23236  lmff  23275  lmcls  23276  lmcnp  23278  fbasssin  23810  flimfil  23943  tgpconncomp  24087  tlmtrg  24164  ustssel  24180  ustincl  24182  ustdiag  24183  ustinvel  24184  ustexhalf  24185  ustfilxp  24187  tustopn  24244  tususp  24245  imasdsf1olem  24347  xmeter  24407  xmetresbl  24411  tmstopn  24459  metustexhalf  24530  nlmnrg  24653  qdensere  24743  blcvx  24772  tgqioo  24774  icccmplem1  24797  icccmplem2  24798  reconnlem1  24801  cnmpopc  24904  iccpnfcnv  24920  phtpcer  24971  phtpcco2  24975  pcohtpy  24996  pcorev2  25004  pcophtb  25005  om1addcl  25009  pi1blem  25015  pi1cpbl  25020  pi1grplem  25025  pi1inv  25028  pi1xfrf  25029  pi1xfr  25031  pi1xfrcnvlem  25032  pi1cof  25035  pi1coghm  25037  cphreccllem  25154  cphsca  25155  cphsubrg  25156  cphsqrtcl2  25162  phclm  25208  tcphcph  25213  lmmcvg  25237  cmetcaulem  25264  lmcau  25289  bcthlem3  25302  bcthlem4  25303  minveclem4c  25401  minveclem2  25402  minveclem3b  25404  minveclem4  25408  minveclem6  25410  ivthicc  25434  ovollb2lem  25464  ovolshftlem1  25485  ovolscalem1  25489  ovolicc1  25492  ovolicc2lem2  25494  ovolicc2lem3  25495  ovolicc2lem4  25496  ovolicc2lem5  25497  ioombl1lem1  25534  dyadmaxlem  25573  volivth  25583  vitalilem2  25585  vitalilem4  25587  i1fima2  25655  itg2monolem1  25726  itgcnlem  25766  itgrevallem1  25771  itgreval  25773  itgle  25786  ibladd  25797  iblabslem  25804  itgspliticc  25813  itgsplitioo  25814  ditgcl  25834  ditgswap  25835  ditgsplitlem  25836  limcdif  25852  limcresi  25861  limcres  25862  limccnp  25867  limccnp2  25868  limcun  25871  dvlip  25970  dvlip2  25972  dveq0  25977  dvgt0lem1  25979  dvivthlem1  25985  dvcnvrelem1  25994  dvcnvre  25996  dvfsumlem2  26005  dvfsumlem2OLD  26006  ftc1lem1  26014  ftc1lem2  26015  ftc1a  26016  ftc1lem4  26018  ftc2  26023  ftc2ditglem  26024  itgsubstlem  26027  ply1rem  26143  fta1glem2  26146  ig1pdvds  26157  plyrem  26284  fta1lem  26286  vieta1lem2  26290  aaliou3lem3  26323  pserulm  26402  psercnlem2  26405  psercnlem1  26406  psercn  26407  pserdvlem1  26408  pserdvlem2  26409  abelth2  26423  coseq00topi  26482  coseq0negpitopi  26483  cosordlem  26510  tanord1  26517  efif1olem1  26522  dvloglem  26628  efopnlem1  26636  logreclem  26743  relogbval  26753  nnlogbexp  26762  logbrec  26763  chordthmlem4  26816  quart1  26837  quartlem2  26839  quartlem3  26840  quart  26842  acosbnd  26881  atancj  26891  atanlogsublem  26896  atantan  26904  atanbndlem  26906  atans2  26912  dvatan  26916  atantayl  26918  divsqrtsumlem  26961  ftalem5  27058  basellem5  27066  ppisval  27085  chtleppi  27192  chpchtsum  27201  chpub  27202  mersenne  27209  perfectlem2  27212  dchrinv  27243  rplogsumlem2  27467  chpdifbndlem1  27535  pntibndlem2  27573  pntlema  27578  pntlemb  27579  pntlemg  27580  pntlemh  27581  pntlemr  27584  pntlemj  27585  pntlemf  27587  pntlemk  27588  pntlemo  27589  pntlemp  27592  pntleml  27593  abvcxp  27597  ostth2lem2  27616  cutsun12  27801  lesrec  27810  eqcuts3  27815  cofcut2  27933  cofcutr  27935  cofcutrtime  27938  cutmax  27945  cutmin  27946  addsproplem5  27984  addsproplem6  27985  leadds1  28000  addsuniflem  28012  addsasslem1  28014  addsasslem2  28015  negsproplem4  28042  negsproplem6  28044  negcut2  28051  negsunif  28066  mulsproplem12  28138  sltmuls1  28158  sltmuls2  28159  mulsuniflem  28160  precsexlem11  28228  twocut  28434  pw2cut2  28473  axtgcont1  28555  cgr3simp3  28609  legso  28686  hlln  28694  hltr  28697  btwnhl  28701  mirhl  28766  mirbtwnhl  28767  opphllem4  28837  opphl  28841  hlpasch  28843  cgracgr  28905  cgraswap  28907  cgrahl  28914  cgracol  28915  inagswap  28928  inagne3  28931  dfcgrg2  28950  umgrnloopv  29194  umgredgne  29233  usgrnloopvALT  29289  frusgrnn0  29660  cusgrm1rusgr  29671  upgrclwlkcompim  29869  2wlkdlem6  30019  2wlkond  30025  2trlond  30027  numclwwlk2lem1  30466  numclwlk2lem2f1o  30469  tncp  30569  grpolidinv  30592  nvs  30754  nvz  30760  nvtri  30761  sspn  30827  minvecolem2  30966  minvecolem4c  30970  minvecolem4  30971  minvecolem5  30972  minvecolem6  30973  adj1  32024  eliccelico  32870  elicoelioo  32871  pmtrto1cl  33180  cyc3evpm  33231  slmdvsdir  33297  slmd0vs  33305  sdrgdvcl  33380  sdrginvcl  33381  nsgqusf1olem3  33495  prmidl  33520  prmidlc  33528  qsidomlem2  33533  qsnzr  33535  mxidlmax  33545  qsdrnglem2  33576  0ringmon1p  33637  ig1pmindeg  33682  ply1degltdimlem  33787  irngss  33852  ply1annig1p  33869  minplycl  33871  algextdeglem3  33884  algextdeglem4  33885  constrsqrtcl  33944  locfinreflem  34005  cnre2csqlem  34075  sigaclci  34297  unelsiga  34299  insiga  34302  unelldsys  34323  ldsysgenld  34325  sigapildsys  34327  ldgenpisyslem1  34328  measvun  34374  cntmeas  34391  sibfima  34503  signstfveq0  34742  tg5segofs  34838  bnj1018g  35126  bnj1018  35127  pfxwlk  35327  revwlk  35328  spthcycl  35332  acycgrcycl  35350  subfacp1lem3  35385  subfacp1lem4  35386  subfacp1lem5  35387  sconnpht2  35441  sconnpi1  35442  txsconn  35444  resconn  35449  cvmcn  35465  cvmsuni  35472  cvmsdisj  35473  cvmshmeo  35474  cvmlift2lem8  35513  cvmlift2lem13  35518  cvmliftphtlem  35520  cvmliftpht  35521  cvmlift3lem6  35527  msrf  35745  elmsta  35751  mthmpps  35785  mclsppslem  35786  ivthALT  36538  weiunfrlem  36667  weiunfr  36670  relowlssretop  37690  ibladdnc  38009  iblabsnclem  38015  ftc2nc  38034  dvasin  38036  isbndx  38114  isbnd3  38116  prdsbnd  38125  heiborlem3  38145  iccbnd  38172  rngohomadd  38301  rngohommul  38302  idladdcl  38351  idllmulcl  38352  idlrmulcl  38353  maxidlmax  38375  pridlc  38403  eqvreltr  39023  lshpnelb  39441  lshpcmp  39445  oplecon3  39656  opnoncon  39665  hlcvl  39816  dochshpncl  41841  lclkrslem1  41994  lclkrslem2  41995  fzne2d  42430  primrootsunit1  42547  primrootscoprmpow  42549  primrootlekpowne0  42555  aks6d1c1p1  42557  aks6d1c2  42580  sticksstones3  42598  aks5lem1  42636  aks5lem2  42637  aks5lem3a  42639  flt4lem5f  43101  flt4lem7  43103  nna4b4nsq  43104  acongrep  43423  ntrneinex  44519  neicvgmex  44559  gneispace0nelrn  44582  cvgdvgrat  44755  binomcxplemdvbinom  44795  eliocre  45954  iccshift  45963  iccsuble  45964  icoiccdif  45969  mullimc  46061  limccog  46065  limciccioolb  46066  mullimcf  46068  limcperiod  46073  lptioo2  46076  lptioo1  46077  neglimc  46090  addlimc  46091  0ellimcdiv  46092  reclimc  46096  xlimmnfvlem1  46275  xlimpnfvlem1  46279  icccncfext  46330  cncfioobdlem  46339  ditgeqiooicc  46403  iblspltprt  46416  iblcncfioo  46421  itgiccshift  46423  itgperiod  46424  itgsbtaddcnst  46425  stoweidlem11  46454  stoweidlem31  46474  stoweidlem36  46479  stoweidlem38  46481  stoweidlem62  46505  dirkercncflem1  46546  dirkercncflem4  46549  fourierdlem26  46576  fourierdlem32  46582  fourierdlem33  46583  fourierdlem37  46587  fourierdlem42  46592  fourierdlem54  46603  fourierdlem63  46612  fourierdlem64  46613  fourierdlem65  46614  fourierdlem74  46623  fourierdlem75  46624  fourierdlem79  46628  fourierdlem81  46630  fourierdlem82  46631  fourierdlem89  46638  fourierdlem90  46639  fourierdlem91  46640  fourierdlem93  46642  fourierdlem101  46650  fourierdlem107  46656  fourierdlem109  46658  fourierdlem111  46660  salunicl  46759  saluncl  46760  hoidmv1lelem1  47034  hoidmv1lelem3  47036  hoidmvlelem1  47038  ovolval3  47090  iinhoiicclem  47116  smfpreimalt  47174  smfpreimaltf  47179  smfpreimale  47197  issmfgt  47199  smfpreimagt  47205  smfpreimage  47225  sigardiv  47304  sigarcol  47307  sharhght  47308  sigaradd  47309  cevathlem1  47310  cevathlem2  47311  cevath  47312  proththd  48074  perfectALTVlem2  48195  gpgnbgrvtx0  48547  gpgnbgrvtx1  48548  imasubc2  49624  imaf1co  49627  idfullsubc  49633  fucofulem1  49782