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  7209  f1dom3el3dif  7210  oeeui  8527  resixp  8867  domssex2  9061  cantnflem1c  9602  cantnflem1  9604  cantnflem3  9606  cantnflem4  9607  fpwwe2lem6  10549  canthnumlem  10561  canthp1lem2  10566  wununi  10619  wunpw  10620  wunpr  10622  lelttrdi  11296  ixxdisj  13281  ixxun  13282  ixxss1  13284  ixxss2  13285  ixxss12  13286  ixxub  13287  ixxlb  13288  lbioo  13297  elicore  13319  iccsupr  13363  icodisj  13397  xov1plusxeqvd  13419  intfracq  13781  fldiv  13782  seqf1olem2  13967  cjmul  15067  icco1  15465  sumtp  15674  rpnnen2lem10  16150  ruclem2  16159  ruclem3  16160  ruclem9  16165  ruclem12  16168  dvdslegcd  16433  prmdvdsbc  16655  crth  16707  eulerthlem1  16710  eulerthlem2  16711  pcpremul  16773  prmreclem2  16847  prmreclem3  16848  4sqlem13  16887  sectcan  17680  sectco  17681  sectmon  17707  monsect  17708  funcid  17795  funcco  17796  funcsect  17797  invfuc  17902  fuciso  17903  coapm  17996  catciso  18036  postr  18244  ipodrsima  18465  psref2  18494  psasym  18500  mhm0  18686  submcl  18704  submmnd  18705  eqger  19075  eqgcpbl  19079  ghmqusnsglem1  19177  ghmquskerlem1  19180  gaorber  19205  orbsta  19210  cayleyth  19312  pmtrrn2  19357  pmtrfinv  19358  pmtrfmvdn0  19359  dfod2  19461  sylow2blem1  19517  sylow2blem3  19519  dprdcntz  19907  dprddisj  19908  dprdffsupp  19913  dpjdisj  19952  ablfac1a  19968  ablfac1b  19969  lmodvsdir  20807  lmhmlin  20957  lbsind  21002  2idlcpblrng  21196  mpfind  22030  mdetunilem2  22516  mdetunilem5  22519  mdetunilem6  22520  mnfnei  23124  cnprcl  23148  lmcvg  23165  lmff  23204  lmcls  23205  lmcnp  23207  fbasssin  23739  flimfil  23872  tgpconncomp  24016  tlmtrg  24093  ustssel  24109  ustincl  24111  ustdiag  24112  ustinvel  24113  ustexhalf  24114  ustfilxp  24116  tustopn  24174  tususp  24175  imasdsf1olem  24277  xmeter  24337  xmetresbl  24341  tmstopn  24389  metustexhalf  24460  nlmnrg  24583  qdensere  24673  blcvx  24702  tgqioo  24704  icccmplem1  24727  icccmplem2  24728  reconnlem1  24731  cnmpopc  24838  iccpnfcnv  24858  phtpcer  24910  phtpcco2  24915  pcohtpy  24936  pcorev2  24944  pcophtb  24945  om1addcl  24949  pi1blem  24955  pi1cpbl  24960  pi1grplem  24965  pi1inv  24968  pi1xfrf  24969  pi1xfr  24971  pi1xfrcnvlem  24972  pi1cof  24975  pi1coghm  24977  cphreccllem  25094  cphsca  25095  cphsubrg  25096  cphsqrtcl2  25102  phclm  25148  tcphcph  25153  lmmcvg  25177  cmetcaulem  25204  lmcau  25229  bcthlem3  25242  bcthlem4  25243  minveclem4c  25341  minveclem2  25342  minveclem3b  25344  minveclem4  25348  minveclem6  25350  ivthicc  25375  ovollb2lem  25405  ovolshftlem1  25426  ovolscalem1  25430  ovolicc1  25433  ovolicc2lem2  25435  ovolicc2lem3  25436  ovolicc2lem4  25437  ovolicc2lem5  25438  ioombl1lem1  25475  dyadmaxlem  25514  volivth  25524  vitalilem2  25526  vitalilem4  25528  i1fima2  25596  itg2monolem1  25667  itgcnlem  25707  itgrevallem1  25712  itgreval  25714  itgle  25727  ibladd  25738  iblabslem  25745  itgspliticc  25754  itgsplitioo  25755  ditgcl  25775  ditgswap  25776  ditgsplitlem  25777  limcdif  25793  limcresi  25802  limcres  25803  limccnp  25808  limccnp2  25809  limcun  25812  dvlip  25914  dvlip2  25916  dveq0  25921  dvgt0lem1  25923  dvivthlem1  25929  dvcnvrelem1  25938  dvcnvre  25940  dvfsumlem2  25949  dvfsumlem2OLD  25950  ftc1lem1  25958  ftc1lem2  25959  ftc1a  25960  ftc1lem4  25962  ftc2  25967  ftc2ditglem  25968  itgsubstlem  25971  ply1rem  26087  fta1glem2  26090  ig1pdvds  26101  plyrem  26229  fta1lem  26231  vieta1lem2  26235  aaliou3lem3  26268  pserulm  26347  psercnlem2  26350  psercnlem1  26351  psercn  26352  pserdvlem1  26353  pserdvlem2  26354  abelth2  26368  coseq00topi  26427  coseq0negpitopi  26428  cosordlem  26455  tanord1  26462  efif1olem1  26467  dvloglem  26573  efopnlem1  26581  logreclem  26688  relogbval  26698  nnlogbexp  26707  logbrec  26708  chordthmlem4  26761  quart1  26782  quartlem2  26784  quartlem3  26785  quart  26787  acosbnd  26826  atancj  26836  atanlogsublem  26841  atantan  26849  atanbndlem  26851  atans2  26857  dvatan  26861  atantayl  26863  divsqrtsumlem  26906  ftalem5  27003  basellem5  27011  ppisval  27030  chtleppi  27137  chpchtsum  27146  chpub  27147  mersenne  27154  perfectlem2  27157  dchrinv  27188  rplogsumlem2  27412  chpdifbndlem1  27480  pntibndlem2  27518  pntlema  27523  pntlemb  27524  pntlemg  27525  pntlemh  27526  pntlemr  27529  pntlemj  27530  pntlemf  27532  pntlemk  27533  pntlemo  27534  pntlemp  27537  pntleml  27538  abvcxp  27542  ostth2lem2  27561  scutun12  27739  slerec  27748  eqscut3  27753  cofcut2  27853  cofcutr  27855  cofcutrtime  27858  cutmax  27865  cutmin  27866  addsproplem5  27903  addsproplem6  27904  sleadd1  27919  addsuniflem  27931  addsasslem1  27933  addsasslem2  27934  negsproplem4  27960  negsproplem6  27962  negscut2  27969  negsunif  27984  mulsproplem12  28053  ssltmul1  28073  ssltmul2  28074  mulsuniflem  28075  precsexlem11  28142  twocut  28333  axtgcont1  28431  cgr3simp3  28485  legso  28562  hlln  28570  hltr  28573  btwnhl  28577  mirhl  28642  mirbtwnhl  28643  opphllem4  28713  opphl  28717  hlpasch  28719  cgracgr  28781  cgraswap  28783  cgrahl  28790  cgracol  28791  inagswap  28804  inagne3  28807  dfcgrg2  28826  umgrnloopv  29069  umgredgne  29108  usgrnloopvALT  29164  frusgrnn0  29535  cusgrm1rusgr  29546  upgrclwlkcompim  29744  2wlkdlem6  29894  2wlkond  29900  2trlond  29902  numclwwlk2lem1  30338  numclwlk2lem2f1o  30341  tncp  30440  grpolidinv  30463  nvs  30625  nvz  30631  nvtri  30632  sspn  30698  minvecolem2  30837  minvecolem4c  30841  minvecolem4  30842  minvecolem5  30843  minvecolem6  30844  adj1  31895  eliccelico  32733  elicoelioo  32734  pmtrto1cl  33054  cyc3evpm  33105  slmdvsdir  33168  slmd0vs  33176  sdrgdvcl  33248  sdrginvcl  33249  nsgqusf1olem3  33362  prmidl  33387  prmidlc  33395  qsidomlem2  33400  qsnzr  33402  mxidlmax  33412  qsdrnglem2  33443  0ringmon1p  33502  ig1pmindeg  33543  ply1degltdimlem  33594  irngss  33658  ply1annig1p  33670  minplycl  33672  algextdeglem3  33685  algextdeglem4  33686  constrsqrtcl  33745  locfinreflem  33806  cnre2csqlem  33876  sigaclci  34098  unelsiga  34100  insiga  34103  unelldsys  34124  ldsysgenld  34126  sigapildsys  34128  ldgenpisyslem1  34129  measvun  34175  cntmeas  34192  sibfima  34305  signstfveq0  34544  tg5segofs  34640  bnj1018g  34929  bnj1018  34930  pfxwlk  35096  revwlk  35097  spthcycl  35101  acycgrcycl  35119  subfacp1lem3  35154  subfacp1lem4  35155  subfacp1lem5  35156  sconnpht2  35210  sconnpi1  35211  txsconn  35213  resconn  35218  cvmcn  35234  cvmsuni  35241  cvmsdisj  35242  cvmshmeo  35243  cvmlift2lem8  35282  cvmlift2lem13  35287  cvmliftphtlem  35289  cvmliftpht  35290  cvmlift3lem6  35296  msrf  35514  elmsta  35520  mthmpps  35554  mclsppslem  35555  ivthALT  36308  weiunfrlem  36437  weiunfr  36440  relowlssretop  37336  ibladdnc  37656  iblabsnclem  37662  ftc2nc  37681  dvasin  37683  isbndx  37761  isbnd3  37763  prdsbnd  37772  heiborlem3  37792  iccbnd  37819  rngohomadd  37948  rngohommul  37949  idladdcl  37998  idllmulcl  37999  idlrmulcl  38000  maxidlmax  38022  pridlc  38050  eqvreltr  38583  lshpnelb  38962  lshpcmp  38966  oplecon3  39177  opnoncon  39186  hlcvl  39337  dochshpncl  41363  lclkrslem1  41516  lclkrslem2  41517  fzne2d  41953  primrootsunit1  42070  primrootscoprmpow  42072  primrootlekpowne0  42078  aks6d1c1p1  42080  aks6d1c2  42103  sticksstones3  42121  aks5lem1  42159  aks5lem2  42160  aks5lem3a  42162  evlsval3  42532  flt4lem5f  42630  flt4lem7  42632  nna4b4nsq  42633  acongrep  42953  ntrneinex  44050  neicvgmex  44090  gneispace0nelrn  44113  cvgdvgrat  44286  binomcxplemdvbinom  44326  eliocre  45491  iccshift  45500  iccsuble  45501  icoiccdif  45506  mullimc  45598  limccog  45602  limciccioolb  45603  mullimcf  45605  limcperiod  45610  lptioo2  45613  lptioo1  45614  neglimc  45629  addlimc  45630  0ellimcdiv  45631  reclimc  45635  xlimmnfvlem1  45814  xlimpnfvlem1  45818  icccncfext  45869  cncfioobdlem  45878  ditgeqiooicc  45942  iblspltprt  45955  iblcncfioo  45960  itgiccshift  45962  itgperiod  45963  itgsbtaddcnst  45964  stoweidlem11  45993  stoweidlem31  46013  stoweidlem36  46018  stoweidlem38  46020  stoweidlem62  46044  dirkercncflem1  46085  dirkercncflem4  46088  fourierdlem26  46115  fourierdlem32  46121  fourierdlem33  46122  fourierdlem37  46126  fourierdlem42  46131  fourierdlem54  46142  fourierdlem63  46151  fourierdlem64  46152  fourierdlem65  46153  fourierdlem74  46162  fourierdlem75  46163  fourierdlem79  46167  fourierdlem81  46169  fourierdlem82  46170  fourierdlem89  46177  fourierdlem90  46178  fourierdlem91  46179  fourierdlem93  46181  fourierdlem101  46189  fourierdlem107  46195  fourierdlem109  46197  fourierdlem111  46199  salunicl  46298  saluncl  46299  hoidmv1lelem1  46573  hoidmv1lelem3  46575  hoidmvlelem1  46577  ovolval3  46629  iinhoiicclem  46655  smfpreimalt  46713  smfpreimaltf  46718  smfpreimale  46736  issmfgt  46738  smfpreimagt  46744  smfpreimage  46764  sigardiv  46843  sigarcol  46846  sharhght  46847  sigaradd  46848  cevathlem1  46849  cevathlem2  46850  cevath  46851  proththd  47599  perfectALTVlem2  47707  gpgnbgrvtx0  48049  gpgnbgrvtx1  48050  imasubc2  49125  imaf1co  49128  idfullsubc  49134  fucofulem1  49283