Theorem simp3d 1156

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  simp3bi  1159  f1dom3fv3dif  7246  f1dom3el3dif  7247  oeeui  8565  resixp  8909  domssex2  9103  cantnflem1c  9637  cantnflem1  9639  cantnflem3  9641  cantnflem4  9642  fpwwe2lem6  10589  canthnumlem  10601  canthp1lem2  10606  wununi  10659  wunpw  10660  wunpr  10662  lelttrdi  11340  ixxdisj  13359  ixxun  13360  ixxss1  13362  ixxss2  13363  ixxss12  13364  ixxub  13365  ixxlb  13366  lbioo  13375  elicore  13397  iccsupr  13441  icodisj  13475  xov1plusxeqvd  13497  intfracq  13864  fldiv  13865  seqf1olem2  14050  cjmul  15150  icco1  15548  sumtp  15757  rpnnen2lem10  16236  ruclem2  16245  ruclem3  16246  ruclem9  16251  ruclem12  16254  dvdslegcd  16519  prmdvdsbc  16742  crth  16794  eulerthlem1  16797  eulerthlem2  16798  pcpremul  16860  prmreclem2  16934  prmreclem3  16935  4sqlem13  16974  sectcan  17769  sectco  17770  sectmon  17796  monsect  17797  funcid  17884  funcco  17885  funcsect  17886  invfuc  17991  fuciso  17992  coapm  18085  catciso  18125  postr  18333  ipodrsima  18554  psref2  18583  psasym  18589  mhm0  18809  submcl  18827  submmnd  18828  eqger  19200  eqgcpbl  19204  ghmqusnsglem1  19301  ghmquskerlem1  19304  gaorber  19329  orbsta  19334  cayleyth  19436  pmtrrn2  19481  pmtrfinv  19482  pmtrfmvdn0  19483  dfod2  19585  sylow2blem1  19641  sylow2blem3  19643  dprdcntz  20031  dprddisj  20032  dprdffsupp  20037  dpjdisj  20076  ablfac1a  20092  ablfac1b  20093  lmodvsdir  20931  lmhmlin  21080  lbsind  21125  2idlcpblrng  21319  evlsval3  22120  mpfind  22146  mdetunilem2  22651  mdetunilem5  22654  mdetunilem6  22655  mnfnei  23259  cnprcl  23283  lmcvg  23300  lmff  23339  lmcls  23340  lmcnp  23342  fbasssin  23874  flimfil  24007  tgpconncomp  24151  tlmtrg  24228  ustssel  24244  ustincl  24246  ustdiag  24247  ustinvel  24248  ustexhalf  24249  ustfilxp  24251  tustopn  24308  tususp  24309  imasdsf1olem  24411  xmeter  24471  xmetresbl  24475  tmstopn  24523  metustexhalf  24594  nlmnrg  24717  qdensere  24807  blcvx  24836  tgqioo  24838  icccmplem1  24861  icccmplem2  24862  reconnlem1  24865  cnmpopc  24968  iccpnfcnv  24984  phtpcer  25035  phtpcco2  25039  pcohtpy  25060  pcorev2  25068  pcophtb  25069  om1addcl  25073  pi1blem  25079  pi1cpbl  25084  pi1grplem  25089  pi1inv  25092  pi1xfrf  25093  pi1xfr  25095  pi1xfrcnvlem  25096  pi1cof  25099  pi1coghm  25101  cphreccllem  25218  cphsca  25219  cphsubrg  25220  cphsqrtcl2  25226  phclm  25272  tcphcph  25277  lmmcvg  25301  cmetcaulem  25328  lmcau  25353  bcthlem3  25366  bcthlem4  25367  minveclem4c  25465  minveclem2  25466  minveclem3b  25468  minveclem4  25472  minveclem6  25474  ivthicc  25498  ovollb2lem  25528  ovolshftlem1  25549  ovolscalem1  25553  ovolicc1  25556  ovolicc2lem2  25558  ovolicc2lem3  25559  ovolicc2lem4  25560  ovolicc2lem5  25561  ioombl1lem1  25598  dyadmaxlem  25637  volivth  25647  vitalilem2  25649  vitalilem4  25651  i1fima2  25719  itg2monolem1  25790  itgcnlem  25830  itgrevallem1  25835  itgreval  25837  itgle  25850  ibladd  25861  iblabslem  25868  itgspliticc  25877  itgsplitioo  25878  ditgcl  25898  ditgswap  25899  ditgsplitlem  25900  limcdif  25916  limcresi  25925  limcres  25926  limccnp  25931  limccnp2  25932  limcun  25935  dvlip  26033  dvlip2  26035  dveq0  26040  dvgt0lem1  26042  dvivthlem1  26048  dvcnvrelem1  26057  dvcnvre  26059  dvfsumlem2  26067  ftc1lem1  26075  ftc1lem2  26076  ftc1a  26077  ftc1lem4  26079  ftc2  26084  ftc2ditglem  26085  itgsubstlem  26088  ply1rem  26204  fta1glem2  26207  ig1pdvds  26218  plyrem  26344  fta1lem  26346  vieta1lem2  26350  aaliou3lem3  26383  pserulm  26460  psercnlem2  26462  psercnlem1  26463  psercn  26464  pserdvlem1  26465  pserdvlem2  26466  abelth2  26480  coseq00topi  26542  coseq0negpitopi  26543  cosordlem  26570  tanord1  26577  efif1olem1  26582  dvloglem  26688  efopnlem1  26696  logreclem  26802  relogbval  26812  nnlogbexp  26821  logbrec  26822  chordthmlem4  26875  quart1  26896  quartlem2  26898  quartlem3  26899  quart  26901  acosbnd  26940  atancj  26950  atanlogsublem  26955  atantan  26963  atanbndlem  26965  atans2  26971  dvatan  26975  atantayl  26977  divsqrtsumlem  27019  ftalem5  27116  basellem5  27124  ppisval  27143  chtleppi  27249  chpchtsum  27258  chpub  27259  mersenne  27266  perfectlem2  27269  dchrinv  27300  rplogsumlem2  27524  chpdifbndlem1  27592  pntibndlem2  27630  pntlema  27635  pntlemb  27636  pntlemg  27637  pntlemh  27638  pntlemr  27641  pntlemj  27642  pntlemf  27644  pntlemk  27645  pntlemo  27646  pntlemp  27649  pntleml  27650  abvcxp  27654  ostth2lem2  27673  cutsun12  27858  lesrec  27867  eqcuts3  27872  cofcut2  27990  cofcutr  27992  cofcutrtime  27995  cutmax  28002  cutmin  28003  addsproplem5  28041  addsproplem6  28042  leadds1  28057  addsuniflem  28069  addsasslem1  28071  addsasslem2  28072  negsproplem4  28099  negsproplem6  28101  negcut2  28108  negsunif  28123  mulsproplem12  28195  sltmuls1  28215  sltmuls2  28216  mulsuniflem  28217  precsexlem11  28285  twocut  28491  pw2cut2  28530  axtgcont1  28612  cgr3simp3  28666  legso  28743  hlln  28751  hltr  28754  btwnhl  28758  mirhl  28823  mirbtwnhl  28824  opphllem4  28894  opphl  28898  hlpasch  28900  cgracgr  28962  cgraswap  28964  cgrahl  28971  cgracol  28972  inagswap  28985  inagne3  28988  dfcgrg2  29007  umgrnloopv  29251  umgredgne  29290  usgrnloopvALT  29346  frusgrnn0  29716  cusgrm1rusgr  29727  upgrclwlkcompim  29925  2wlkdlem6  30075  2wlkond  30081  2trlond  30083  numclwwlk2lem1  30522  numclwlk2lem2f1o  30525  tncp  30625  grpolidinv  30648  nvs  30810  nvz  30816  nvtri  30817  sspn  30883  minvecolem2  31022  minvecolem4c  31026  minvecolem4  31027  minvecolem5  31028  minvecolem6  31029  adj1  32080  eliccelico  32927  elicoelioo  32928  pmtrto1cl  33238  cyc3evpm  33289  slmdvsdir  33355  slmd0vs  33363  sdrgdvcl  33445  sdrginvcl  33446  nsgqusf1olem3  33560  prmidl  33585  prmidlc  33593  prmidlprop  33594  qsidomlem2  33599  qsnzr  33601  mxidlmax  33612  qsdrnglem2  33643  0ringmon1p  33712  ig1pmindeg  33757  ply1degltdimlem  33878  irngss  33943  ply1annig1p  33960  minplycl  33962  algextdeglem3  33975  algextdeglem4  33976  constrsqrtcl  34035  locfinreflem  34096  cnre2csqlem  34166  sigaclci  34388  unelsiga  34390  insiga  34393  unelldsys  34414  ldsysgenld  34416  sigapildsys  34418  ldgenpisyslem1  34419  measvun  34465  cntmeas  34482  sibfima  34594  signstfveq0  34833  cgranbtwn  34925  tg5segofs  34932  bnj1018g  35220  bnj1018  35221  pfxwlk  35427  revwlk  35428  spthcycl  35432  acycgrcycl  35450  subfacp1lem3  35485  subfacp1lem4  35486  subfacp1lem5  35487  sconnpht2  35541  sconnpi1  35542  txsconn  35544  resconn  35549  cvmcn  35565  cvmsuni  35572  cvmsdisj  35573  cvmshmeo  35574  cvmlift2lem8  35613  cvmlift2lem13  35618  cvmliftphtlem  35620  cvmliftpht  35621  cvmlift3lem6  35627  msrf  35845  elmsta  35851  mthmpps  35885  mclsppslem  35886  ivthALT  36648  weiunfrlem  36777  weiunfr  36780  relowlssretop  37810  ibladdnc  38129  iblabsnclem  38135  ftc2nc  38154  dvasin  38156  isbndx  38234  isbnd3  38236  prdsbnd  38245  heiborlem3  38265  iccbnd  38292  rngohomadd  38421  rngohommul  38422  idladdcl  38471  idllmulcl  38472  idlrmulcl  38473  maxidlmax  38495  pridlc  38523  eqvreltr  39143  lshpnelb  39561  lshpcmp  39565  oplecon3  39776  opnoncon  39785  hlcvl  39936  dochshpncl  41961  lclkrslem1  42114  lclkrslem2  42115  fzne2d  42550  primrootsunit1  42667  primrootscoprmpow  42669  primrootlekpowne0  42675  aks6d1c1p1  42677  aks6d1c2  42700  sticksstones3  42718  aks5lem1  42756  aks5lem2  42757  aks5lem3a  42759  flt4lem5f  43192  flt4lem7  43194  nna4b4nsq  43195  acongrep  43510  ntrneinex  44606  neicvgmex  44646  gneispace0nelrn  44669  cvgdvgrat  44842  binomcxplemdvbinom  44882  eliocre  46038  iccshift  46047  iccsuble  46048  icoiccdif  46053  mullimc  46145  limccog  46149  limciccioolb  46150  mullimcf  46152  limcperiod  46157  lptioo2  46160  lptioo1  46161  neglimc  46174  addlimc  46175  0ellimcdiv  46176  reclimc  46180  xlimmnfvlem1  46359  xlimpnfvlem1  46363  icccncfext  46414  cncfioobdlem  46423  ditgeqiooicc  46487  iblspltprt  46500  iblcncfioo  46505  itgiccshift  46507  itgperiod  46508  itgsbtaddcnst  46509  stoweidlem11  46538  stoweidlem31  46558  stoweidlem36  46563  stoweidlem38  46565  stoweidlem62  46589  dirkercncflem1  46630  dirkercncflem4  46633  fourierdlem26  46660  fourierdlem32  46666  fourierdlem33  46667  fourierdlem37  46671  fourierdlem42  46676  fourierdlem54  46687  fourierdlem63  46696  fourierdlem64  46697  fourierdlem65  46698  fourierdlem74  46707  fourierdlem75  46708  fourierdlem79  46712  fourierdlem81  46714  fourierdlem82  46715  fourierdlem89  46722  fourierdlem90  46723  fourierdlem91  46724  fourierdlem93  46726  fourierdlem101  46734  fourierdlem107  46740  fourierdlem109  46742  fourierdlem111  46744  salunicl  46843  saluncl  46844  hoidmv1lelem1  47118  hoidmv1lelem3  47120  hoidmvlelem1  47122  ovolval3  47174  iinhoiicclem  47200  smfpreimalt  47258  smfpreimaltf  47263  smfpreimale  47281  issmfgt  47283  smfpreimagt  47289  smfpreimage  47309  sigardiv  47388  sigarcol  47391  sharhght  47392  sigaradd  47393  cevathlem1  47394  cevathlem2  47395  cevath  47396  proththd  48176  perfectALTVlem2  48297  gpgnbgrvtx0  48649  gpgnbgrvtx1  48650  imasubc2  49726  imaf1co  49729  idfullsubc  49735  fucofulem1  49884