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  7246  f1dom3el3dif  7247  oeeui  8569  resixp  8909  domssex2  9107  cantnflem1c  9647  cantnflem1  9649  cantnflem3  9651  cantnflem4  9652  fpwwe2lem6  10596  canthnumlem  10608  canthp1lem2  10613  wununi  10666  wunpw  10667  wunpr  10669  lelttrdi  11343  ixxdisj  13328  ixxun  13329  ixxss1  13331  ixxss2  13332  ixxss12  13333  ixxub  13334  ixxlb  13335  lbioo  13344  elicore  13366  iccsupr  13410  icodisj  13444  xov1plusxeqvd  13466  intfracq  13828  fldiv  13829  seqf1olem2  14014  cjmul  15115  icco1  15513  sumtp  15722  rpnnen2lem10  16198  ruclem2  16207  ruclem3  16208  ruclem9  16213  ruclem12  16216  dvdslegcd  16481  prmdvdsbc  16703  crth  16755  eulerthlem1  16758  eulerthlem2  16759  pcpremul  16821  prmreclem2  16895  prmreclem3  16896  4sqlem13  16935  sectcan  17724  sectco  17725  sectmon  17751  monsect  17752  funcid  17839  funcco  17840  funcsect  17841  invfuc  17946  fuciso  17947  coapm  18040  catciso  18080  postr  18288  ipodrsima  18507  psref2  18536  psasym  18542  mhm0  18728  submcl  18746  submmnd  18747  eqger  19117  eqgcpbl  19121  ghmqusnsglem1  19219  ghmquskerlem1  19222  gaorber  19247  orbsta  19252  cayleyth  19352  pmtrrn2  19397  pmtrfinv  19398  pmtrfmvdn0  19399  dfod2  19501  sylow2blem1  19557  sylow2blem3  19559  dprdcntz  19947  dprddisj  19948  dprdffsupp  19953  dpjdisj  19992  ablfac1a  20008  ablfac1b  20009  lmodvsdir  20799  lmhmlin  20949  lbsind  20994  2idlcpblrng  21188  mpfind  22021  mdetunilem2  22507  mdetunilem5  22510  mdetunilem6  22511  mnfnei  23115  cnprcl  23139  lmcvg  23156  lmff  23195  lmcls  23196  lmcnp  23198  fbasssin  23730  flimfil  23863  tgpconncomp  24007  tlmtrg  24084  ustssel  24100  ustincl  24102  ustdiag  24103  ustinvel  24104  ustexhalf  24105  ustfilxp  24107  tustopn  24165  tususp  24166  imasdsf1olem  24268  xmeter  24328  xmetresbl  24332  tmstopn  24380  metustexhalf  24451  nlmnrg  24574  qdensere  24664  blcvx  24693  tgqioo  24695  icccmplem1  24718  icccmplem2  24719  reconnlem1  24722  cnmpopc  24829  iccpnfcnv  24849  phtpcer  24901  phtpcco2  24906  pcohtpy  24927  pcorev2  24935  pcophtb  24936  om1addcl  24940  pi1blem  24946  pi1cpbl  24951  pi1grplem  24956  pi1inv  24959  pi1xfrf  24960  pi1xfr  24962  pi1xfrcnvlem  24963  pi1cof  24966  pi1coghm  24968  cphreccllem  25085  cphsca  25086  cphsubrg  25087  cphsqrtcl2  25093  phclm  25139  tcphcph  25144  lmmcvg  25168  cmetcaulem  25195  lmcau  25220  bcthlem3  25233  bcthlem4  25234  minveclem4c  25332  minveclem2  25333  minveclem3b  25335  minveclem4  25339  minveclem6  25341  ivthicc  25366  ovollb2lem  25396  ovolshftlem1  25417  ovolscalem1  25421  ovolicc1  25424  ovolicc2lem2  25426  ovolicc2lem3  25427  ovolicc2lem4  25428  ovolicc2lem5  25429  ioombl1lem1  25466  dyadmaxlem  25505  volivth  25515  vitalilem2  25517  vitalilem4  25519  i1fima2  25587  itg2monolem1  25658  itgcnlem  25698  itgrevallem1  25703  itgreval  25705  itgle  25718  ibladd  25729  iblabslem  25736  itgspliticc  25745  itgsplitioo  25746  ditgcl  25766  ditgswap  25767  ditgsplitlem  25768  limcdif  25784  limcresi  25793  limcres  25794  limccnp  25799  limccnp2  25800  limcun  25803  dvlip  25905  dvlip2  25907  dveq0  25912  dvgt0lem1  25914  dvivthlem1  25920  dvcnvrelem1  25929  dvcnvre  25931  dvfsumlem2  25940  dvfsumlem2OLD  25941  ftc1lem1  25949  ftc1lem2  25950  ftc1a  25951  ftc1lem4  25953  ftc2  25958  ftc2ditglem  25959  itgsubstlem  25962  ply1rem  26078  fta1glem2  26081  ig1pdvds  26092  plyrem  26220  fta1lem  26222  vieta1lem2  26226  aaliou3lem3  26259  pserulm  26338  psercnlem2  26341  psercnlem1  26342  psercn  26343  pserdvlem1  26344  pserdvlem2  26345  abelth2  26359  coseq00topi  26418  coseq0negpitopi  26419  cosordlem  26446  tanord1  26453  efif1olem1  26458  dvloglem  26564  efopnlem1  26572  logreclem  26679  relogbval  26689  nnlogbexp  26698  logbrec  26699  chordthmlem4  26752  quart1  26773  quartlem2  26775  quartlem3  26776  quart  26778  acosbnd  26817  atancj  26827  atanlogsublem  26832  atantan  26840  atanbndlem  26842  atans2  26848  dvatan  26852  atantayl  26854  divsqrtsumlem  26897  ftalem5  26994  basellem5  27002  ppisval  27021  chtleppi  27128  chpchtsum  27137  chpub  27138  mersenne  27145  perfectlem2  27148  dchrinv  27179  rplogsumlem2  27403  chpdifbndlem1  27471  pntibndlem2  27509  pntlema  27514  pntlemb  27515  pntlemg  27516  pntlemh  27517  pntlemr  27520  pntlemj  27521  pntlemf  27523  pntlemk  27524  pntlemo  27525  pntlemp  27528  pntleml  27529  abvcxp  27533  ostth2lem2  27552  scutun12  27729  slerec  27738  cofcut2  27837  cofcutr  27839  cofcutrtime  27842  cutmax  27849  cutmin  27850  addsproplem5  27887  addsproplem6  27888  sleadd1  27903  addsuniflem  27915  addsasslem1  27917  addsasslem2  27918  negsproplem4  27944  negsproplem6  27946  negscut2  27953  negsunif  27968  mulsproplem12  28037  ssltmul1  28057  ssltmul2  28058  mulsuniflem  28059  precsexlem11  28126  twocut  28316  axtgcont1  28402  cgr3simp3  28456  legso  28533  hlln  28541  hltr  28544  btwnhl  28548  mirhl  28613  mirbtwnhl  28614  opphllem4  28684  opphl  28688  hlpasch  28690  cgracgr  28752  cgraswap  28754  cgrahl  28761  cgracol  28762  inagswap  28775  inagne3  28778  dfcgrg2  28797  umgrnloopv  29040  umgredgne  29079  usgrnloopvALT  29135  frusgrnn0  29506  cusgrm1rusgr  29517  upgrclwlkcompim  29718  2wlkdlem6  29868  2wlkond  29874  2trlond  29876  numclwwlk2lem1  30312  numclwlk2lem2f1o  30315  tncp  30414  grpolidinv  30437  nvs  30599  nvz  30605  nvtri  30606  sspn  30672  minvecolem2  30811  minvecolem4c  30815  minvecolem4  30816  minvecolem5  30817  minvecolem6  30818  adj1  31869  eliccelico  32707  elicoelioo  32708  pmtrto1cl  33063  cyc3evpm  33114  slmdvsdir  33176  slmd0vs  33184  sdrgdvcl  33256  sdrginvcl  33257  nsgqusf1olem3  33393  prmidl  33418  prmidlc  33426  qsidomlem2  33431  qsnzr  33433  mxidlmax  33443  qsdrnglem2  33474  0ringmon1p  33533  ig1pmindeg  33574  ply1degltdimlem  33625  irngss  33689  ply1annig1p  33701  minplycl  33703  algextdeglem3  33716  algextdeglem4  33717  constrsqrtcl  33776  locfinreflem  33837  cnre2csqlem  33907  sigaclci  34129  unelsiga  34131  insiga  34134  unelldsys  34155  ldsysgenld  34157  sigapildsys  34159  ldgenpisyslem1  34160  measvun  34206  cntmeas  34223  sibfima  34336  signstfveq0  34575  tg5segofs  34671  bnj1018g  34960  bnj1018  34961  pfxwlk  35118  revwlk  35119  spthcycl  35123  acycgrcycl  35141  subfacp1lem3  35176  subfacp1lem4  35177  subfacp1lem5  35178  sconnpht2  35232  sconnpi1  35233  txsconn  35235  resconn  35240  cvmcn  35256  cvmsuni  35263  cvmsdisj  35264  cvmshmeo  35265  cvmlift2lem8  35304  cvmlift2lem13  35309  cvmliftphtlem  35311  cvmliftpht  35312  cvmlift3lem6  35318  msrf  35536  elmsta  35542  mthmpps  35576  mclsppslem  35577  ivthALT  36330  weiunfrlem  36459  weiunfr  36462  relowlssretop  37358  ibladdnc  37678  iblabsnclem  37684  ftc2nc  37703  dvasin  37705  isbndx  37783  isbnd3  37785  prdsbnd  37794  heiborlem3  37814  iccbnd  37841  rngohomadd  37970  rngohommul  37971  idladdcl  38020  idllmulcl  38021  idlrmulcl  38022  maxidlmax  38044  pridlc  38072  eqvreltr  38605  lshpnelb  38984  lshpcmp  38988  oplecon3  39199  opnoncon  39208  hlcvl  39359  dochshpncl  41385  lclkrslem1  41538  lclkrslem2  41539  fzne2d  41975  primrootsunit1  42092  primrootscoprmpow  42094  primrootlekpowne0  42100  aks6d1c1p1  42102  aks6d1c2  42125  sticksstones3  42143  aks5lem1  42181  aks5lem2  42182  aks5lem3a  42184  evlsval3  42554  flt4lem5f  42652  flt4lem7  42654  nna4b4nsq  42655  acongrep  42976  ntrneinex  44073  neicvgmex  44113  gneispace0nelrn  44136  cvgdvgrat  44309  binomcxplemdvbinom  44349  eliocre  45514  iccshift  45523  iccsuble  45524  icoiccdif  45529  mullimc  45621  limccog  45625  limciccioolb  45626  mullimcf  45628  limcperiod  45633  lptioo2  45636  lptioo1  45637  neglimc  45652  addlimc  45653  0ellimcdiv  45654  reclimc  45658  xlimmnfvlem1  45837  xlimpnfvlem1  45841  icccncfext  45892  cncfioobdlem  45901  ditgeqiooicc  45965  iblspltprt  45978  iblcncfioo  45983  itgiccshift  45985  itgperiod  45986  itgsbtaddcnst  45987  stoweidlem11  46016  stoweidlem31  46036  stoweidlem36  46041  stoweidlem38  46043  stoweidlem62  46067  dirkercncflem1  46108  dirkercncflem4  46111  fourierdlem26  46138  fourierdlem32  46144  fourierdlem33  46145  fourierdlem37  46149  fourierdlem42  46154  fourierdlem54  46165  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem74  46185  fourierdlem75  46186  fourierdlem79  46190  fourierdlem81  46192  fourierdlem82  46193  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem93  46204  fourierdlem101  46212  fourierdlem107  46218  fourierdlem109  46220  fourierdlem111  46222  salunicl  46321  saluncl  46322  hoidmv1lelem1  46596  hoidmv1lelem3  46598  hoidmvlelem1  46600  ovolval3  46652  iinhoiicclem  46678  smfpreimalt  46736  smfpreimaltf  46741  smfpreimale  46759  issmfgt  46761  smfpreimagt  46767  smfpreimage  46787  sigardiv  46866  sigarcol  46869  sharhght  46870  sigaradd  46871  cevathlem1  46872  cevathlem2  46873  cevath  46874  proththd  47619  perfectALTVlem2  47727  gpgnbgrvtx0  48069  gpgnbgrvtx1  48070  imasubc2  49145  imaf1co  49148  idfullsubc  49154  fucofulem1  49303