Theorem simp3d 1144

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp3bi  1147  f1dom3fv3dif  7243  f1dom3el3dif  7244  oeeui  8566  resixp  8906  domssex2  9101  cantnflem1c  9640  cantnflem1  9642  cantnflem3  9644  cantnflem4  9645  fpwwe2lem6  10589  canthnumlem  10601  canthp1lem2  10606  wununi  10659  wunpw  10660  wunpr  10662  lelttrdi  11336  ixxdisj  13321  ixxun  13322  ixxss1  13324  ixxss2  13325  ixxss12  13326  ixxub  13327  ixxlb  13328  lbioo  13337  elicore  13359  iccsupr  13403  icodisj  13437  xov1plusxeqvd  13459  intfracq  13821  fldiv  13822  seqf1olem2  14007  cjmul  15108  icco1  15506  sumtp  15715  rpnnen2lem10  16191  ruclem2  16200  ruclem3  16201  ruclem9  16206  ruclem12  16209  dvdslegcd  16474  prmdvdsbc  16696  crth  16748  eulerthlem1  16751  eulerthlem2  16752  pcpremul  16814  prmreclem2  16888  prmreclem3  16889  4sqlem13  16928  sectcan  17717  sectco  17718  sectmon  17744  monsect  17745  funcid  17832  funcco  17833  funcsect  17834  invfuc  17939  fuciso  17940  coapm  18033  catciso  18073  postr  18281  ipodrsima  18500  psref2  18529  psasym  18535  mhm0  18721  submcl  18739  submmnd  18740  eqger  19110  eqgcpbl  19114  ghmqusnsglem1  19212  ghmquskerlem1  19215  gaorber  19240  orbsta  19245  cayleyth  19345  pmtrrn2  19390  pmtrfinv  19391  pmtrfmvdn0  19392  dfod2  19494  sylow2blem1  19550  sylow2blem3  19552  dprdcntz  19940  dprddisj  19941  dprdffsupp  19946  dpjdisj  19985  ablfac1a  20001  ablfac1b  20002  lmodvsdir  20792  lmhmlin  20942  lbsind  20987  2idlcpblrng  21181  mpfind  22014  mdetunilem2  22500  mdetunilem5  22503  mdetunilem6  22504  mnfnei  23108  cnprcl  23132  lmcvg  23149  lmff  23188  lmcls  23189  lmcnp  23191  fbasssin  23723  flimfil  23856  tgpconncomp  24000  tlmtrg  24077  ustssel  24093  ustincl  24095  ustdiag  24096  ustinvel  24097  ustexhalf  24098  ustfilxp  24100  tustopn  24158  tususp  24159  imasdsf1olem  24261  xmeter  24321  xmetresbl  24325  tmstopn  24373  metustexhalf  24444  nlmnrg  24567  qdensere  24657  blcvx  24686  tgqioo  24688  icccmplem1  24711  icccmplem2  24712  reconnlem1  24715  cnmpopc  24822  iccpnfcnv  24842  phtpcer  24894  phtpcco2  24899  pcohtpy  24920  pcorev2  24928  pcophtb  24929  om1addcl  24933  pi1blem  24939  pi1cpbl  24944  pi1grplem  24949  pi1inv  24952  pi1xfrf  24953  pi1xfr  24955  pi1xfrcnvlem  24956  pi1cof  24959  pi1coghm  24961  cphreccllem  25078  cphsca  25079  cphsubrg  25080  cphsqrtcl2  25086  phclm  25132  tcphcph  25137  lmmcvg  25161  cmetcaulem  25188  lmcau  25213  bcthlem3  25226  bcthlem4  25227  minveclem4c  25325  minveclem2  25326  minveclem3b  25328  minveclem4  25332  minveclem6  25334  ivthicc  25359  ovollb2lem  25389  ovolshftlem1  25410  ovolscalem1  25414  ovolicc1  25417  ovolicc2lem2  25419  ovolicc2lem3  25420  ovolicc2lem4  25421  ovolicc2lem5  25422  ioombl1lem1  25459  dyadmaxlem  25498  volivth  25508  vitalilem2  25510  vitalilem4  25512  i1fima2  25580  itg2monolem1  25651  itgcnlem  25691  itgrevallem1  25696  itgreval  25698  itgle  25711  ibladd  25722  iblabslem  25729  itgspliticc  25738  itgsplitioo  25739  ditgcl  25759  ditgswap  25760  ditgsplitlem  25761  limcdif  25777  limcresi  25786  limcres  25787  limccnp  25792  limccnp2  25793  limcun  25796  dvlip  25898  dvlip2  25900  dveq0  25905  dvgt0lem1  25907  dvivthlem1  25913  dvcnvrelem1  25922  dvcnvre  25924  dvfsumlem2  25933  dvfsumlem2OLD  25934  ftc1lem1  25942  ftc1lem2  25943  ftc1a  25944  ftc1lem4  25946  ftc2  25951  ftc2ditglem  25952  itgsubstlem  25955  ply1rem  26071  fta1glem2  26074  ig1pdvds  26085  plyrem  26213  fta1lem  26215  vieta1lem2  26219  aaliou3lem3  26252  pserulm  26331  psercnlem2  26334  psercnlem1  26335  psercn  26336  pserdvlem1  26337  pserdvlem2  26338  abelth2  26352  coseq00topi  26411  coseq0negpitopi  26412  cosordlem  26439  tanord1  26446  efif1olem1  26451  dvloglem  26557  efopnlem1  26565  logreclem  26672  relogbval  26682  nnlogbexp  26691  logbrec  26692  chordthmlem4  26745  quart1  26766  quartlem2  26768  quartlem3  26769  quart  26771  acosbnd  26810  atancj  26820  atanlogsublem  26825  atantan  26833  atanbndlem  26835  atans2  26841  dvatan  26845  atantayl  26847  divsqrtsumlem  26890  ftalem5  26987  basellem5  26995  ppisval  27014  chtleppi  27121  chpchtsum  27130  chpub  27131  mersenne  27138  perfectlem2  27141  dchrinv  27172  rplogsumlem2  27396  chpdifbndlem1  27464  pntibndlem2  27502  pntlema  27507  pntlemb  27508  pntlemg  27509  pntlemh  27510  pntlemr  27513  pntlemj  27514  pntlemf  27516  pntlemk  27517  pntlemo  27518  pntlemp  27521  pntleml  27522  abvcxp  27526  ostth2lem2  27545  scutun12  27722  slerec  27731  cofcut2  27830  cofcutr  27832  cofcutrtime  27835  cutmax  27842  cutmin  27843  addsproplem5  27880  addsproplem6  27881  sleadd1  27896  addsuniflem  27908  addsasslem1  27910  addsasslem2  27911  negsproplem4  27937  negsproplem6  27939  negscut2  27946  negsunif  27961  mulsproplem12  28030  ssltmul1  28050  ssltmul2  28051  mulsuniflem  28052  precsexlem11  28119  twocut  28309  axtgcont1  28395  cgr3simp3  28449  legso  28526  hlln  28534  hltr  28537  btwnhl  28541  mirhl  28606  mirbtwnhl  28607  opphllem4  28677  opphl  28681  hlpasch  28683  cgracgr  28745  cgraswap  28747  cgrahl  28754  cgracol  28755  inagswap  28768  inagne3  28771  dfcgrg2  28790  umgrnloopv  29033  umgredgne  29072  usgrnloopvALT  29128  frusgrnn0  29499  cusgrm1rusgr  29510  upgrclwlkcompim  29711  2wlkdlem6  29861  2wlkond  29867  2trlond  29869  numclwwlk2lem1  30305  numclwlk2lem2f1o  30308  tncp  30407  grpolidinv  30430  nvs  30592  nvz  30598  nvtri  30599  sspn  30665  minvecolem2  30804  minvecolem4c  30808  minvecolem4  30809  minvecolem5  30810  minvecolem6  30811  adj1  31862  eliccelico  32700  elicoelioo  32701  pmtrto1cl  33056  cyc3evpm  33107  slmdvsdir  33169  slmd0vs  33177  sdrgdvcl  33249  sdrginvcl  33250  nsgqusf1olem3  33386  prmidl  33411  prmidlc  33419  qsidomlem2  33424  qsnzr  33426  mxidlmax  33436  qsdrnglem2  33467  0ringmon1p  33526  ig1pmindeg  33567  ply1degltdimlem  33618  irngss  33682  ply1annig1p  33694  minplycl  33696  algextdeglem3  33709  algextdeglem4  33710  constrsqrtcl  33769  locfinreflem  33830  cnre2csqlem  33900  sigaclci  34122  unelsiga  34124  insiga  34127  unelldsys  34148  ldsysgenld  34150  sigapildsys  34152  ldgenpisyslem1  34153  measvun  34199  cntmeas  34216  sibfima  34329  signstfveq0  34568  tg5segofs  34664  bnj1018g  34953  bnj1018  34954  pfxwlk  35111  revwlk  35112  spthcycl  35116  acycgrcycl  35134  subfacp1lem3  35169  subfacp1lem4  35170  subfacp1lem5  35171  sconnpht2  35225  sconnpi1  35226  txsconn  35228  resconn  35233  cvmcn  35249  cvmsuni  35256  cvmsdisj  35257  cvmshmeo  35258  cvmlift2lem8  35297  cvmlift2lem13  35302  cvmliftphtlem  35304  cvmliftpht  35305  cvmlift3lem6  35311  msrf  35529  elmsta  35535  mthmpps  35569  mclsppslem  35570  ivthALT  36323  weiunfrlem  36452  weiunfr  36455  relowlssretop  37351  ibladdnc  37671  iblabsnclem  37677  ftc2nc  37696  dvasin  37698  isbndx  37776  isbnd3  37778  prdsbnd  37787  heiborlem3  37807  iccbnd  37834  rngohomadd  37963  rngohommul  37964  idladdcl  38013  idllmulcl  38014  idlrmulcl  38015  maxidlmax  38037  pridlc  38065  eqvreltr  38598  lshpnelb  38977  lshpcmp  38981  oplecon3  39192  opnoncon  39201  hlcvl  39352  dochshpncl  41378  lclkrslem1  41531  lclkrslem2  41532  fzne2d  41968  primrootsunit1  42085  primrootscoprmpow  42087  primrootlekpowne0  42093  aks6d1c1p1  42095  aks6d1c2  42118  sticksstones3  42136  aks5lem1  42174  aks5lem2  42175  aks5lem3a  42177  evlsval3  42547  flt4lem5f  42645  flt4lem7  42647  nna4b4nsq  42648  acongrep  42969  ntrneinex  44066  neicvgmex  44106  gneispace0nelrn  44129  cvgdvgrat  44302  binomcxplemdvbinom  44342  eliocre  45507  iccshift  45516  iccsuble  45517  icoiccdif  45522  mullimc  45614  limccog  45618  limciccioolb  45619  mullimcf  45621  limcperiod  45626  lptioo2  45629  lptioo1  45630  neglimc  45645  addlimc  45646  0ellimcdiv  45647  reclimc  45651  xlimmnfvlem1  45830  xlimpnfvlem1  45834  icccncfext  45885  cncfioobdlem  45894  ditgeqiooicc  45958  iblspltprt  45971  iblcncfioo  45976  itgiccshift  45978  itgperiod  45979  itgsbtaddcnst  45980  stoweidlem11  46009  stoweidlem31  46029  stoweidlem36  46034  stoweidlem38  46036  stoweidlem62  46060  dirkercncflem1  46101  dirkercncflem4  46104  fourierdlem26  46131  fourierdlem32  46137  fourierdlem33  46138  fourierdlem37  46142  fourierdlem42  46147  fourierdlem54  46158  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem74  46178  fourierdlem75  46179  fourierdlem79  46183  fourierdlem81  46185  fourierdlem82  46186  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem93  46197  fourierdlem101  46205  fourierdlem107  46211  fourierdlem109  46213  fourierdlem111  46215  salunicl  46314  saluncl  46315  hoidmv1lelem1  46589  hoidmv1lelem3  46591  hoidmvlelem1  46593  ovolval3  46645  iinhoiicclem  46671  smfpreimalt  46729  smfpreimaltf  46734  smfpreimale  46752  issmfgt  46754  smfpreimagt  46760  smfpreimage  46780  sigardiv  46859  sigarcol  46862  sharhght  46863  sigaradd  46864  cevathlem1  46865  cevathlem2  46866  cevath  46867  proththd  47615  perfectALTVlem2  47723  gpgnbgrvtx0  48065  gpgnbgrvtx1  48066  imasubc2  49141  imaf1co  49144  idfullsubc  49150  fucofulem1  49299