Theorem simp3d 1160

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 1154	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1101

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

This theorem is referenced by:  simp3bi  1163  f1dom3fv3dif  7266  f1dom3el3dif  7267  oeeui  8587  resixp  8930  domssex2  9124  cantnflem1c  9655  cantnflem1  9657  cantnflem3  9659  cantnflem4  9660  fpwwe2lem6  10620  canthnumlem  10632  canthp1lem2  10637  wununi  10690  wunpw  10691  wunpr  10693  lelttrdi  11371  ixxdisj  13386  ixxun  13387  ixxss1  13389  ixxss2  13390  ixxss12  13391  ixxub  13392  ixxlb  13393  lbioo  13402  elicore  13424  iccsupr  13468  icodisj  13502  xov1plusxeqvd  13524  intfracq  13892  fldiv  13893  seqf1olem2  14078  cjmul  15193  icco1  15591  sumtp  15800  rpnnen2lem10  16278  ruclem2  16287  ruclem3  16288  ruclem9  16293  ruclem12  16296  dvdslegcd  16561  prmdvdsbc  16784  crth  16836  eulerthlem1  16839  eulerthlem2  16840  pcpremul  16902  prmreclem2  16976  prmreclem3  16977  4sqlem13  17016  sectcan  17811  sectco  17812  sectmon  17838  monsect  17839  funcid  17926  funcco  17927  funcsect  17928  invfuc  18033  fuciso  18034  coapm  18127  catciso  18167  postr  18375  ipodrsima  18596  psref2  18625  psasym  18631  mhm0  18851  submcl  18869  submmnd  18871  eqger  19245  eqgcpbl  19249  ghmqusnsglem1  19349  ghmquskerlem1  19352  gaorber  19377  orbsta  19382  cayleyth  19484  pmtrrn2  19529  pmtrfinv  19530  pmtrfmvdn0  19531  dfod2  19633  sylow2blem1  19689  sylow2blem3  19691  dprdcntz  20079  dprddisj  20080  dprdffsupp  20085  dpjdisj  20124  ablfac1a  20140  ablfac1b  20141  lmodvsdir  20986  lmhmlin  21135  lbsind  21180  2idlcpblrng  21389  prmidl  21444  prmidlc  21452  prmidlprop  21455  qsidomlem2  21460  qsnzr  21462  evlsval3  22219  mpfind  22245  mdetunilem2  22749  mdetunilem5  22752  mdetunilem6  22753  mnfnei  23357  cnprcl  23381  lmcvg  23398  lmff  23437  lmcls  23438  lmcnp  23440  fbasssin  23972  flimfil  24105  tgpconncomp  24249  tlmtrg  24326  ustssel  24342  ustincl  24344  ustdiag  24345  ustinvel  24346  ustexhalf  24347  ustfilxp  24349  tustopn  24406  tususp  24407  imasdsf1olem  24509  xmeter  24569  xmetresbl  24573  tmstopn  24621  metustexhalf  24692  nlmnrg  24815  qdensere  24905  blcvx  24934  tgqioo  24936  icccmplem1  24959  icccmplem2  24960  reconnlem1  24963  cnmpopc  25066  iccpnfcnv  25082  phtpcer  25133  phtpcco2  25137  pcohtpy  25158  pcorev2  25166  pcophtb  25167  om1addcl  25171  pi1blem  25177  pi1cpbl  25182  pi1grplem  25187  pi1inv  25190  pi1xfrf  25191  pi1xfr  25193  pi1xfrcnvlem  25194  pi1cof  25197  pi1coghm  25199  cphreccllem  25316  cphsca  25317  cphsubrg  25318  cphsqrtcl2  25324  phclm  25370  tcphcph  25375  lmmcvg  25399  cmetcaulem  25426  lmcau  25451  bcthlem3  25464  bcthlem4  25465  minveclem4c  25563  minveclem2  25564  minveclem3b  25566  minveclem4  25570  minveclem6  25572  ivthicc  25596  ovollb2lem  25626  ovolshftlem1  25647  ovolscalem1  25651  ovolicc1  25654  ovolicc2lem2  25656  ovolicc2lem3  25657  ovolicc2lem4  25658  ovolicc2lem5  25659  ioombl1lem1  25696  dyadmaxlem  25735  volivth  25745  vitalilem2  25747  vitalilem4  25749  i1fima2  25817  itg2monolem1  25888  itgcnlem  25928  itgrevallem1  25933  itgreval  25935  itgle  25948  ibladd  25959  iblabslem  25966  itgspliticc  25975  itgsplitioo  25976  ditgcl  25996  ditgswap  25997  ditgsplitlem  25998  limcdif  26014  limcresi  26023  limcres  26024  limccnp  26029  limccnp2  26030  limcun  26033  dvlip  26131  dvlip2  26133  dveq0  26138  dvgt0lem1  26140  dvivthlem1  26146  dvcnvrelem1  26155  dvcnvre  26157  dvfsumlem2  26165  ftc1lem1  26173  ftc1lem2  26174  ftc1a  26175  ftc1lem4  26177  ftc2  26182  ftc2ditglem  26183  itgsubstlem  26186  ply1rem  26302  fta1glem2  26305  ig1pdvds  26316  plyrem  26445  fta1lem  26447  vieta1lem2  26451  aaliou3lem3  26484  pserulm  26561  psercnlem2  26563  psercnlem1  26564  psercn  26565  pserdvlem1  26566  pserdvlem2  26567  abelth2  26581  coseq00topi  26643  coseq0negpitopi  26644  cosordlem  26671  tanord1  26678  efif1olem1  26683  dvloglem  26789  efopnlem1  26797  logreclem  26903  relogbval  26913  nnlogbexp  26922  logbrec  26923  chordthmlem4  26976  quart1  26997  quartlem2  26999  quartlem3  27000  quart  27002  acosbnd  27041  atancj  27051  atanlogsublem  27056  atantan  27064  atanbndlem  27066  atans2  27072  dvatan  27076  atantayl  27078  divsqrtsumlem  27120  ftalem5  27217  basellem5  27225  ppisval  27244  chtleppi  27350  chpchtsum  27359  chpub  27360  mersenne  27367  perfectlem2  27370  dchrinv  27401  rplogsumlem2  27625  chpdifbndlem1  27693  pntibndlem2  27731  pntlema  27736  pntlemb  27737  pntlemg  27738  pntlemh  27739  pntlemr  27742  pntlemj  27743  pntlemf  27745  pntlemk  27746  pntlemo  27747  pntlemp  27750  pntleml  27751  abvcxp  27755  ostth2lem2  27774  cutsun12  27959  lesrec  27968  eqcuts3  27973  cofcut2  28091  cofcutr  28093  cofcutrtime  28096  cutmax  28103  cutmin  28104  addsproplem5  28142  addsproplem6  28143  leadds1  28158  addsuniflem  28170  addsasslem1  28172  addsasslem2  28173  negsproplem4  28200  negsproplem6  28202  negcut2  28209  negsunif  28224  mulsproplem12  28296  sltmuls1  28316  sltmuls2  28317  mulsuniflem  28318  precsexlem11  28386  twocut  28592  pw2cut2  28631  axtgcont1  28713  cgr3simp3  28767  legso  28844  hlln  28855  hltr  28858  btwnhl  28862  mirhl  28932  mirbtwnhl  28933  opphllem4  29006  opphl  29010  hlpasch  29013  cgracgr  29102  cgraswap  29104  cgrahl  29111  cgracol  29112  inagswap  29131  inagne3  29134  dfcgrg2  29153  umgrnloopv  29422  umgredgne  29461  usgrnloopvALT  29517  frusgrnn0  29887  cusgrm1rusgr  29898  upgrclwlkcompim  30096  2wlkdlem6  30246  2wlkond  30252  2trlond  30254  numclwwlk2lem1  30693  numclwlk2lem2f1o  30696  tncp  30796  grpolidinv  30819  nvs  30981  nvz  30987  nvtri  30988  sspn  31054  minvecolem2  31193  minvecolem4c  31197  minvecolem4  31198  minvecolem5  31199  minvecolem6  31200  adj1  32251  eliccelico  33088  elicoelioo  33089  pmtrto1cl  33385  cyc3evpm  33436  slmdvsdir  33502  slmd0vs  33510  sdrgdvcl  33586  sdrginvcl  33587  nsgqusf1olem3  33690  mxidlmax  33714  qsdrnglem2  33744  0ringmon1p  33813  ig1pmindeg  33858  ply1degltdimlem  33978  irngss  34043  ply1annig1p  34060  minplycl  34062  algextdeglem3  34075  algextdeglem4  34076  constrsqrtcl  34135  locfinreflem  34196  cnre2csqlem  34266  sigaclci  34488  unelsiga  34490  insiga  34493  unelldsys  34514  ldsysgenld  34516  sigapildsys  34518  ldgenpisyslem1  34519  measvun  34565  cntmeas  34582  sibfima  34694  signstfveq0  34930  cgranbtwn  35022  tg5segofs  35029  bnj1018g  35317  bnj1018  35318  pfxwlk  35582  revwlk  35583  spthcycl  35587  acycgrcycl  35605  subfacp1lem3  35640  subfacp1lem4  35641  subfacp1lem5  35642  sconnpht2  35696  sconnpi1  35697  txsconn  35699  resconn  35704  cvmcn  35720  cvmsuni  35727  cvmsdisj  35728  cvmshmeo  35729  cvmlift2lem8  35768  cvmlift2lem13  35773  cvmliftphtlem  35775  cvmliftpht  35776  cvmlift3lem6  35782  msrf  36000  elmsta  36006  mthmpps  36040  mclsppslem  36041  ivthALT  36812  weiunfrlem  36941  weiunfr  36944  relowlssretop  37975  ibladdnc  38294  iblabsnclem  38300  ftc2nc  38319  dvasin  38321  isbndx  38399  isbnd3  38401  prdsbnd  38410  heiborlem3  38430  iccbnd  38457  rngohomadd  38586  rngohommul  38587  idladdcl  38636  idllmulcl  38637  idlrmulcl  38638  maxidlmax  38660  pridlc  38688  eqvreltr  39308  lshpnelb  39726  lshpcmp  39730  oplecon3  39941  opnoncon  39950  hlcvl  40101  dochshpncl  42126  lclkrslem1  42279  lclkrslem2  42280  fzne2d  42715  primrootsunit1  42832  primrootscoprmpow  42834  primrootlekpowne0  42840  aks6d1c1p1  42842  aks6d1c2  42865  sticksstones3  42883  aks5lem1  42921  aks5lem2  42922  aks5lem3a  42924  flt4lem5f  43359  flt4lem7  43361  nna4b4nsq  43362  acongrep  43677  ntrneinex  44773  neicvgmex  44813  gneispace0nelrn  44836  cvgdvgrat  44993  binomcxplemdvbinom  45033  eliocre  46195  iccshift  46204  iccsuble  46205  icoiccdif  46210  mullimc  46302  limccog  46306  limciccioolb  46307  mullimcf  46309  limcperiod  46314  lptioo2  46317  lptioo1  46318  neglimc  46331  addlimc  46332  0ellimcdiv  46333  reclimc  46337  xlimmnfvlem1  46516  xlimpnfvlem1  46520  icccncfext  46571  cncfioobdlem  46580  ditgeqiooicc  46644  iblspltprt  46657  iblcncfioo  46662  itgiccshift  46664  itgperiod  46665  itgsbtaddcnst  46666  stoweidlem11  46695  stoweidlem31  46715  stoweidlem36  46720  stoweidlem38  46722  stoweidlem62  46746  dirkercncflem1  46787  dirkercncflem4  46790  fourierdlem26  46817  fourierdlem32  46823  fourierdlem33  46824  fourierdlem37  46828  fourierdlem42  46833  fourierdlem54  46844  fourierdlem63  46853  fourierdlem64  46854  fourierdlem65  46855  fourierdlem74  46864  fourierdlem75  46865  fourierdlem79  46869  fourierdlem81  46871  fourierdlem82  46872  fourierdlem89  46879  fourierdlem90  46880  fourierdlem91  46881  fourierdlem93  46883  fourierdlem101  46891  fourierdlem107  46897  fourierdlem109  46899  fourierdlem111  46901  salunicl  47000  saluncl  47001  hoidmv1lelem1  47275  hoidmv1lelem3  47277  hoidmvlelem1  47279  ovolval3  47331  iinhoiicclem  47357  smfpreimalt  47415  smfpreimaltf  47420  smfpreimale  47438  issmfgt  47440  smfpreimagt  47446  smfpreimage  47466  sigardiv  47545  sigarcol  47548  sharhght  47549  sigaradd  47550  cevathlem1  47551  cevathlem2  47552  cevath  47553  proththd  48333  perfectALTVlem2  48454  gpgnbgrvtx0  48806  gpgnbgrvtx1  48807  imasubc2  49897  imaf1co  49900  idfullsubc  49906  fucofulem1  50055