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  7197  f1dom3el3dif  7198  oeeui  8512  resixp  8852  domssex2  9045  cantnflem1c  9572  cantnflem1  9574  cantnflem3  9576  cantnflem4  9577  fpwwe2lem6  10519  canthnumlem  10531  canthp1lem2  10536  wununi  10589  wunpw  10590  wunpr  10592  lelttrdi  11267  ixxdisj  13252  ixxun  13253  ixxss1  13255  ixxss2  13256  ixxss12  13257  ixxub  13258  ixxlb  13259  lbioo  13268  elicore  13290  iccsupr  13334  icodisj  13368  xov1plusxeqvd  13390  intfracq  13755  fldiv  13756  seqf1olem2  13941  cjmul  15041  icco1  15439  sumtp  15648  rpnnen2lem10  16124  ruclem2  16133  ruclem3  16134  ruclem9  16139  ruclem12  16142  dvdslegcd  16407  prmdvdsbc  16629  crth  16681  eulerthlem1  16684  eulerthlem2  16685  pcpremul  16747  prmreclem2  16821  prmreclem3  16822  4sqlem13  16861  sectcan  17654  sectco  17655  sectmon  17681  monsect  17682  funcid  17769  funcco  17770  funcsect  17771  invfuc  17876  fuciso  17877  coapm  17970  catciso  18010  postr  18218  ipodrsima  18439  psref2  18468  psasym  18474  mhm0  18694  submcl  18712  submmnd  18713  eqger  19083  eqgcpbl  19087  ghmqusnsglem1  19185  ghmquskerlem1  19188  gaorber  19213  orbsta  19218  cayleyth  19320  pmtrrn2  19365  pmtrfinv  19366  pmtrfmvdn0  19367  dfod2  19469  sylow2blem1  19525  sylow2blem3  19527  dprdcntz  19915  dprddisj  19916  dprdffsupp  19921  dpjdisj  19960  ablfac1a  19976  ablfac1b  19977  lmodvsdir  20812  lmhmlin  20962  lbsind  21007  2idlcpblrng  21201  mpfind  22035  mdetunilem2  22521  mdetunilem5  22524  mdetunilem6  22525  mnfnei  23129  cnprcl  23153  lmcvg  23170  lmff  23209  lmcls  23210  lmcnp  23212  fbasssin  23744  flimfil  23877  tgpconncomp  24021  tlmtrg  24098  ustssel  24114  ustincl  24116  ustdiag  24117  ustinvel  24118  ustexhalf  24119  ustfilxp  24121  tustopn  24178  tususp  24179  imasdsf1olem  24281  xmeter  24341  xmetresbl  24345  tmstopn  24393  metustexhalf  24464  nlmnrg  24587  qdensere  24677  blcvx  24706  tgqioo  24708  icccmplem1  24731  icccmplem2  24732  reconnlem1  24735  cnmpopc  24842  iccpnfcnv  24862  phtpcer  24914  phtpcco2  24919  pcohtpy  24940  pcorev2  24948  pcophtb  24949  om1addcl  24953  pi1blem  24959  pi1cpbl  24964  pi1grplem  24969  pi1inv  24972  pi1xfrf  24973  pi1xfr  24975  pi1xfrcnvlem  24976  pi1cof  24979  pi1coghm  24981  cphreccllem  25098  cphsca  25099  cphsubrg  25100  cphsqrtcl2  25106  phclm  25152  tcphcph  25157  lmmcvg  25181  cmetcaulem  25208  lmcau  25233  bcthlem3  25246  bcthlem4  25247  minveclem4c  25345  minveclem2  25346  minveclem3b  25348  minveclem4  25352  minveclem6  25354  ivthicc  25379  ovollb2lem  25409  ovolshftlem1  25430  ovolscalem1  25434  ovolicc1  25437  ovolicc2lem2  25439  ovolicc2lem3  25440  ovolicc2lem4  25441  ovolicc2lem5  25442  ioombl1lem1  25479  dyadmaxlem  25518  volivth  25528  vitalilem2  25530  vitalilem4  25532  i1fima2  25600  itg2monolem1  25671  itgcnlem  25711  itgrevallem1  25716  itgreval  25718  itgle  25731  ibladd  25742  iblabslem  25749  itgspliticc  25758  itgsplitioo  25759  ditgcl  25779  ditgswap  25780  ditgsplitlem  25781  limcdif  25797  limcresi  25806  limcres  25807  limccnp  25812  limccnp2  25813  limcun  25816  dvlip  25918  dvlip2  25920  dveq0  25925  dvgt0lem1  25927  dvivthlem1  25933  dvcnvrelem1  25942  dvcnvre  25944  dvfsumlem2  25953  dvfsumlem2OLD  25954  ftc1lem1  25962  ftc1lem2  25963  ftc1a  25964  ftc1lem4  25966  ftc2  25971  ftc2ditglem  25972  itgsubstlem  25975  ply1rem  26091  fta1glem2  26094  ig1pdvds  26105  plyrem  26233  fta1lem  26235  vieta1lem2  26239  aaliou3lem3  26272  pserulm  26351  psercnlem2  26354  psercnlem1  26355  psercn  26356  pserdvlem1  26357  pserdvlem2  26358  abelth2  26372  coseq00topi  26431  coseq0negpitopi  26432  cosordlem  26459  tanord1  26466  efif1olem1  26471  dvloglem  26577  efopnlem1  26585  logreclem  26692  relogbval  26702  nnlogbexp  26711  logbrec  26712  chordthmlem4  26765  quart1  26786  quartlem2  26788  quartlem3  26789  quart  26791  acosbnd  26830  atancj  26840  atanlogsublem  26845  atantan  26853  atanbndlem  26855  atans2  26861  dvatan  26865  atantayl  26867  divsqrtsumlem  26910  ftalem5  27007  basellem5  27015  ppisval  27034  chtleppi  27141  chpchtsum  27150  chpub  27151  mersenne  27158  perfectlem2  27161  dchrinv  27192  rplogsumlem2  27416  chpdifbndlem1  27484  pntibndlem2  27522  pntlema  27527  pntlemb  27528  pntlemg  27529  pntlemh  27530  pntlemr  27533  pntlemj  27534  pntlemf  27536  pntlemk  27537  pntlemo  27538  pntlemp  27541  pntleml  27542  abvcxp  27546  ostth2lem2  27565  scutun12  27744  slerec  27753  eqscut3  27758  cofcut2  27859  cofcutr  27861  cofcutrtime  27864  cutmax  27871  cutmin  27872  addsproplem5  27909  addsproplem6  27910  sleadd1  27925  addsuniflem  27937  addsasslem1  27939  addsasslem2  27940  negsproplem4  27966  negsproplem6  27968  negscut2  27975  negsunif  27990  mulsproplem12  28059  ssltmul1  28079  ssltmul2  28080  mulsuniflem  28081  precsexlem11  28148  twocut  28339  pw2cut2  28375  axtgcont1  28439  cgr3simp3  28493  legso  28570  hlln  28578  hltr  28581  btwnhl  28585  mirhl  28650  mirbtwnhl  28651  opphllem4  28721  opphl  28725  hlpasch  28727  cgracgr  28789  cgraswap  28791  cgrahl  28798  cgracol  28799  inagswap  28812  inagne3  28815  dfcgrg2  28834  umgrnloopv  29077  umgredgne  29116  usgrnloopvALT  29172  frusgrnn0  29543  cusgrm1rusgr  29554  upgrclwlkcompim  29752  2wlkdlem6  29902  2wlkond  29908  2trlond  29910  numclwwlk2lem1  30346  numclwlk2lem2f1o  30349  tncp  30448  grpolidinv  30471  nvs  30633  nvz  30639  nvtri  30640  sspn  30706  minvecolem2  30845  minvecolem4c  30849  minvecolem4  30850  minvecolem5  30851  minvecolem6  30852  adj1  31903  eliccelico  32750  elicoelioo  32751  pmtrto1cl  33058  cyc3evpm  33109  slmdvsdir  33175  slmd0vs  33183  sdrgdvcl  33255  sdrginvcl  33256  nsgqusf1olem3  33370  prmidl  33395  prmidlc  33403  qsidomlem2  33408  qsnzr  33410  mxidlmax  33420  qsdrnglem2  33451  0ringmon1p  33510  ig1pmindeg  33552  ply1degltdimlem  33625  irngss  33690  ply1annig1p  33707  minplycl  33709  algextdeglem3  33722  algextdeglem4  33723  constrsqrtcl  33782  locfinreflem  33843  cnre2csqlem  33913  sigaclci  34135  unelsiga  34137  insiga  34140  unelldsys  34161  ldsysgenld  34163  sigapildsys  34165  ldgenpisyslem1  34166  measvun  34212  cntmeas  34229  sibfima  34341  signstfveq0  34580  tg5segofs  34676  bnj1018g  34965  bnj1018  34966  pfxwlk  35136  revwlk  35137  spthcycl  35141  acycgrcycl  35159  subfacp1lem3  35194  subfacp1lem4  35195  subfacp1lem5  35196  sconnpht2  35250  sconnpi1  35251  txsconn  35253  resconn  35258  cvmcn  35274  cvmsuni  35281  cvmsdisj  35282  cvmshmeo  35283  cvmlift2lem8  35322  cvmlift2lem13  35327  cvmliftphtlem  35329  cvmliftpht  35330  cvmlift3lem6  35336  msrf  35554  elmsta  35560  mthmpps  35594  mclsppslem  35595  ivthALT  36348  weiunfrlem  36477  weiunfr  36480  relowlssretop  37376  ibladdnc  37696  iblabsnclem  37702  ftc2nc  37721  dvasin  37723  isbndx  37801  isbnd3  37803  prdsbnd  37812  heiborlem3  37832  iccbnd  37859  rngohomadd  37988  rngohommul  37989  idladdcl  38038  idllmulcl  38039  idlrmulcl  38040  maxidlmax  38062  pridlc  38090  eqvreltr  38623  lshpnelb  39002  lshpcmp  39006  oplecon3  39217  opnoncon  39226  hlcvl  39377  dochshpncl  41402  lclkrslem1  41555  lclkrslem2  41556  fzne2d  41992  primrootsunit1  42109  primrootscoprmpow  42111  primrootlekpowne0  42117  aks6d1c1p1  42119  aks6d1c2  42142  sticksstones3  42160  aks5lem1  42198  aks5lem2  42199  aks5lem3a  42201  evlsval3  42571  flt4lem5f  42669  flt4lem7  42671  nna4b4nsq  42672  acongrep  42992  ntrneinex  44089  neicvgmex  44129  gneispace0nelrn  44152  cvgdvgrat  44325  binomcxplemdvbinom  44365  eliocre  45528  iccshift  45537  iccsuble  45538  icoiccdif  45543  mullimc  45635  limccog  45639  limciccioolb  45640  mullimcf  45642  limcperiod  45647  lptioo2  45650  lptioo1  45651  neglimc  45664  addlimc  45665  0ellimcdiv  45666  reclimc  45670  xlimmnfvlem1  45849  xlimpnfvlem1  45853  icccncfext  45904  cncfioobdlem  45913  ditgeqiooicc  45977  iblspltprt  45990  iblcncfioo  45995  itgiccshift  45997  itgperiod  45998  itgsbtaddcnst  45999  stoweidlem11  46028  stoweidlem31  46048  stoweidlem36  46053  stoweidlem38  46055  stoweidlem62  46079  dirkercncflem1  46120  dirkercncflem4  46123  fourierdlem26  46150  fourierdlem32  46156  fourierdlem33  46157  fourierdlem37  46161  fourierdlem42  46166  fourierdlem54  46177  fourierdlem63  46186  fourierdlem64  46187  fourierdlem65  46188  fourierdlem74  46197  fourierdlem75  46198  fourierdlem79  46202  fourierdlem81  46204  fourierdlem82  46205  fourierdlem89  46212  fourierdlem90  46213  fourierdlem91  46214  fourierdlem93  46216  fourierdlem101  46224  fourierdlem107  46230  fourierdlem109  46232  fourierdlem111  46234  salunicl  46333  saluncl  46334  hoidmv1lelem1  46608  hoidmv1lelem3  46610  hoidmvlelem1  46612  ovolval3  46664  iinhoiicclem  46690  smfpreimalt  46748  smfpreimaltf  46753  smfpreimale  46771  issmfgt  46773  smfpreimagt  46779  smfpreimage  46799  sigardiv  46878  sigarcol  46881  sharhght  46882  sigaradd  46883  cevathlem1  46884  cevathlem2  46885  cevath  46886  proththd  47624  perfectALTVlem2  47732  gpgnbgrvtx0  48084  gpgnbgrvtx1  48085  imasubc2  49163  imaf1co  49166  idfullsubc  49172  fucofulem1  49321