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  7260  f1dom3el3dif  7261  oeeui  8612  resixp  8945  domssex2  9149  cantnflem1c  9699  cantnflem1  9701  cantnflem3  9703  cantnflem4  9704  fpwwe2lem6  10648  canthnumlem  10660  canthp1lem2  10665  wununi  10718  wunpw  10719  wunpr  10721  lelttrdi  11395  ixxdisj  13375  ixxun  13376  ixxss1  13378  ixxss2  13379  ixxss12  13380  ixxub  13381  ixxlb  13382  lbioo  13391  elicore  13413  iccsupr  13457  icodisj  13491  xov1plusxeqvd  13513  intfracq  13874  fldiv  13875  seqf1olem2  14058  cjmul  15159  icco1  15554  sumtp  15763  rpnnen2lem10  16239  ruclem2  16248  ruclem3  16249  ruclem9  16254  ruclem12  16257  dvdslegcd  16521  prmdvdsbc  16743  crth  16795  eulerthlem1  16798  eulerthlem2  16799  pcpremul  16861  prmreclem2  16935  prmreclem3  16936  4sqlem13  16975  sectcan  17766  sectco  17767  sectmon  17793  monsect  17794  funcid  17881  funcco  17882  funcsect  17883  invfuc  17988  fuciso  17989  coapm  18082  catciso  18122  postr  18330  ipodrsima  18549  psref2  18578  psasym  18584  mhm0  18770  submcl  18788  submmnd  18789  eqger  19159  eqgcpbl  19163  ghmqusnsglem1  19261  ghmquskerlem1  19264  gaorber  19289  orbsta  19294  cayleyth  19394  pmtrrn2  19439  pmtrfinv  19440  pmtrfmvdn0  19441  dfod2  19543  sylow2blem1  19599  sylow2blem3  19601  dprdcntz  19989  dprddisj  19990  dprdffsupp  19995  dpjdisj  20034  ablfac1a  20050  ablfac1b  20051  lmodvsdir  20841  lmhmlin  20991  lbsind  21036  2idlcpblrng  21230  mpfind  22063  mdetunilem2  22549  mdetunilem5  22552  mdetunilem6  22553  mnfnei  23157  cnprcl  23181  lmcvg  23198  lmff  23237  lmcls  23238  lmcnp  23240  fbasssin  23772  flimfil  23905  tgpconncomp  24049  tlmtrg  24126  ustssel  24142  ustincl  24144  ustdiag  24145  ustinvel  24146  ustexhalf  24147  ustfilxp  24149  tustopn  24207  tususp  24208  imasdsf1olem  24310  xmeter  24370  xmetresbl  24374  tmstopn  24422  metustexhalf  24493  nlmnrg  24616  qdensere  24706  blcvx  24735  tgqioo  24737  icccmplem1  24760  icccmplem2  24761  reconnlem1  24764  cnmpopc  24871  iccpnfcnv  24891  phtpcer  24943  phtpcco2  24948  pcohtpy  24969  pcorev2  24977  pcophtb  24978  om1addcl  24982  pi1blem  24988  pi1cpbl  24993  pi1grplem  24998  pi1inv  25001  pi1xfrf  25002  pi1xfr  25004  pi1xfrcnvlem  25005  pi1cof  25008  pi1coghm  25010  cphreccllem  25128  cphsca  25129  cphsubrg  25130  cphsqrtcl2  25136  phclm  25182  tcphcph  25187  lmmcvg  25211  cmetcaulem  25238  lmcau  25263  bcthlem3  25276  bcthlem4  25277  minveclem4c  25375  minveclem2  25376  minveclem3b  25378  minveclem4  25382  minveclem6  25384  ivthicc  25409  ovollb2lem  25439  ovolshftlem1  25460  ovolscalem1  25464  ovolicc1  25467  ovolicc2lem2  25469  ovolicc2lem3  25470  ovolicc2lem4  25471  ovolicc2lem5  25472  ioombl1lem1  25509  dyadmaxlem  25548  volivth  25558  vitalilem2  25560  vitalilem4  25562  i1fima2  25630  itg2monolem1  25701  itgcnlem  25741  itgrevallem1  25746  itgreval  25748  itgle  25761  ibladd  25772  iblabslem  25779  itgspliticc  25788  itgsplitioo  25789  ditgcl  25809  ditgswap  25810  ditgsplitlem  25811  limcdif  25827  limcresi  25836  limcres  25837  limccnp  25842  limccnp2  25843  limcun  25846  dvlip  25948  dvlip2  25950  dveq0  25955  dvgt0lem1  25957  dvivthlem1  25963  dvcnvrelem1  25972  dvcnvre  25974  dvfsumlem2  25983  dvfsumlem2OLD  25984  ftc1lem1  25992  ftc1lem2  25993  ftc1a  25994  ftc1lem4  25996  ftc2  26001  ftc2ditglem  26002  itgsubstlem  26005  ply1rem  26121  fta1glem2  26124  ig1pdvds  26135  plyrem  26263  fta1lem  26265  vieta1lem2  26269  aaliou3lem3  26302  pserulm  26381  psercnlem2  26384  psercnlem1  26385  psercn  26386  pserdvlem1  26387  pserdvlem2  26388  abelth2  26402  coseq00topi  26461  coseq0negpitopi  26462  cosordlem  26489  tanord1  26496  efif1olem1  26501  dvloglem  26607  efopnlem1  26615  logreclem  26722  relogbval  26732  nnlogbexp  26741  logbrec  26742  chordthmlem4  26795  quart1  26816  quartlem2  26818  quartlem3  26819  quart  26821  acosbnd  26860  atancj  26870  atanlogsublem  26875  atantan  26883  atanbndlem  26885  atans2  26891  dvatan  26895  atantayl  26897  divsqrtsumlem  26940  ftalem5  27037  basellem5  27045  ppisval  27064  chtleppi  27171  chpchtsum  27180  chpub  27181  mersenne  27188  perfectlem2  27191  dchrinv  27222  rplogsumlem2  27446  chpdifbndlem1  27514  pntibndlem2  27552  pntlema  27557  pntlemb  27558  pntlemg  27559  pntlemh  27560  pntlemr  27563  pntlemj  27564  pntlemf  27566  pntlemk  27567  pntlemo  27568  pntlemp  27571  pntleml  27572  abvcxp  27576  ostth2lem2  27595  scutun12  27772  slerec  27781  cofcut2  27873  cofcutr  27875  cofcutrtime  27878  cutmax  27885  cutmin  27886  addsproplem5  27923  addsproplem6  27924  sleadd1  27939  addsuniflem  27951  addsasslem1  27953  addsasslem2  27954  negsproplem4  27980  negsproplem6  27982  negscut2  27989  negsunif  28004  mulsproplem12  28070  ssltmul1  28090  ssltmul2  28091  mulsuniflem  28092  precsexlem11  28158  axtgcont1  28393  cgr3simp3  28447  legso  28524  hlln  28532  hltr  28535  btwnhl  28539  mirhl  28604  mirbtwnhl  28605  opphllem4  28675  opphl  28679  hlpasch  28681  cgracgr  28743  cgraswap  28745  cgrahl  28752  cgracol  28753  inagswap  28766  inagne3  28769  dfcgrg2  28788  umgrnloopv  29031  umgredgne  29070  usgrnloopvALT  29126  frusgrnn0  29497  cusgrm1rusgr  29508  upgrclwlkcompim  29709  2wlkdlem6  29859  2wlkond  29865  2trlond  29867  numclwwlk2lem1  30303  numclwlk2lem2f1o  30306  tncp  30405  grpolidinv  30428  nvs  30590  nvz  30596  nvtri  30597  sspn  30663  minvecolem2  30802  minvecolem4c  30806  minvecolem4  30807  minvecolem5  30808  minvecolem6  30809  adj1  31860  eliccelico  32700  elicoelioo  32701  pmtrto1cl  33056  cyc3evpm  33107  slmdvsdir  33159  slmd0vs  33167  sdrgdvcl  33239  sdrginvcl  33240  nsgqusf1olem3  33376  prmidl  33401  prmidlc  33409  qsidomlem2  33414  qsnzr  33416  mxidlmax  33426  qsdrnglem2  33457  0ringmon1p  33516  ig1pmindeg  33557  ply1degltdimlem  33608  irngss  33674  ply1annig1p  33684  minplycl  33686  algextdeglem3  33699  algextdeglem4  33700  constrsqrtcl  33759  locfinreflem  33817  cnre2csqlem  33887  sigaclci  34109  unelsiga  34111  insiga  34114  unelldsys  34135  ldsysgenld  34137  sigapildsys  34139  ldgenpisyslem1  34140  measvun  34186  cntmeas  34203  sibfima  34316  signstfveq0  34555  tg5segofs  34651  bnj1018g  34940  bnj1018  34941  pfxwlk  35092  revwlk  35093  spthcycl  35097  acycgrcycl  35115  subfacp1lem3  35150  subfacp1lem4  35151  subfacp1lem5  35152  sconnpht2  35206  sconnpi1  35207  txsconn  35209  resconn  35214  cvmcn  35230  cvmsuni  35237  cvmsdisj  35238  cvmshmeo  35239  cvmlift2lem8  35278  cvmlift2lem13  35283  cvmliftphtlem  35285  cvmliftpht  35286  cvmlift3lem6  35292  msrf  35510  elmsta  35516  mthmpps  35550  mclsppslem  35551  ivthALT  36299  weiunfrlem  36428  weiunfr  36431  relowlssretop  37327  ibladdnc  37647  iblabsnclem  37653  ftc2nc  37672  dvasin  37674  isbndx  37752  isbnd3  37754  prdsbnd  37763  heiborlem3  37783  iccbnd  37810  rngohomadd  37939  rngohommul  37940  idladdcl  37989  idllmulcl  37990  idlrmulcl  37991  maxidlmax  38013  pridlc  38041  eqvreltr  38571  lshpnelb  38948  lshpcmp  38952  oplecon3  39163  opnoncon  39172  hlcvl  39323  dochshpncl  41349  lclkrslem1  41502  lclkrslem2  41503  fzne2d  41939  primrootsunit1  42056  primrootscoprmpow  42058  primrootlekpowne0  42064  aks6d1c1p1  42066  aks6d1c2  42089  sticksstones3  42107  aks5lem1  42145  aks5lem2  42146  aks5lem3a  42148  metakunt8  42171  metakunt20  42183  metakunt21  42184  metakunt22  42185  metakunt24  42187  metakunt25  42188  evlsval3  42529  flt4lem5f  42627  flt4lem7  42629  nna4b4nsq  42630  acongrep  42951  ntrneinex  44048  neicvgmex  44088  gneispace0nelrn  44111  cvgdvgrat  44285  binomcxplemdvbinom  44325  eliocre  45486  iccshift  45495  iccsuble  45496  icoiccdif  45501  mullimc  45593  limccog  45597  limciccioolb  45598  mullimcf  45600  limcperiod  45605  lptioo2  45608  lptioo1  45609  neglimc  45624  addlimc  45625  0ellimcdiv  45626  reclimc  45630  xlimmnfvlem1  45809  xlimpnfvlem1  45813  icccncfext  45864  cncfioobdlem  45873  ditgeqiooicc  45937  iblspltprt  45950  iblcncfioo  45955  itgiccshift  45957  itgperiod  45958  itgsbtaddcnst  45959  stoweidlem11  45988  stoweidlem31  46008  stoweidlem36  46013  stoweidlem38  46015  stoweidlem62  46039  dirkercncflem1  46080  dirkercncflem4  46083  fourierdlem26  46110  fourierdlem32  46116  fourierdlem33  46117  fourierdlem37  46121  fourierdlem42  46126  fourierdlem54  46137  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem74  46157  fourierdlem75  46158  fourierdlem79  46162  fourierdlem81  46164  fourierdlem82  46165  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem93  46176  fourierdlem101  46184  fourierdlem107  46190  fourierdlem109  46192  fourierdlem111  46194  salunicl  46293  saluncl  46294  hoidmv1lelem1  46568  hoidmv1lelem3  46570  hoidmvlelem1  46572  ovolval3  46624  iinhoiicclem  46650  smfpreimalt  46708  smfpreimaltf  46713  smfpreimale  46731  issmfgt  46733  smfpreimagt  46739  smfpreimage  46759  sigardiv  46838  sigarcol  46841  sharhght  46842  sigaradd  46843  cevathlem1  46844  cevathlem2  46845  cevath  46846  proththd  47576  perfectALTVlem2  47684  gpgnbgrvtx0  48024  gpgnbgrvtx1  48025  imasubc2  49040  imaf1co  49043  idfullsubc  49048  fucofulem1  49169