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 1087

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 1089

This theorem is referenced by:  simp3bi  1147  f1dom3fv3dif  7305  f1dom3el3dif  7306  oeeui  8658  resixp  8991  domssex2  9203  cantnflem1c  9756  cantnflem1  9758  cantnflem3  9760  cantnflem4  9761  fpwwe2lem6  10705  canthnumlem  10717  canthp1lem2  10722  wununi  10775  wunpw  10776  wunpr  10778  lelttrdi  11452  ixxdisj  13422  ixxun  13423  ixxss1  13425  ixxss2  13426  ixxss12  13427  ixxub  13428  ixxlb  13429  lbioo  13438  elicore  13459  iccsupr  13502  icodisj  13536  xov1plusxeqvd  13558  intfracq  13910  fldiv  13911  seqf1olem2  14093  cjmul  15191  icco1  15586  sumtp  15797  rpnnen2lem10  16271  ruclem2  16280  ruclem3  16281  ruclem9  16286  ruclem12  16289  dvdslegcd  16550  prmdvdsbc  16773  crth  16825  eulerthlem1  16828  eulerthlem2  16829  pcpremul  16890  prmreclem2  16964  prmreclem3  16965  4sqlem13  17004  sectcan  17816  sectco  17817  sectmon  17843  monsect  17844  funcid  17934  funcco  17935  funcsect  17936  invfuc  18044  fuciso  18045  coapm  18138  catciso  18178  postr  18390  ipodrsima  18611  psref2  18640  psasym  18646  mhm0  18829  submcl  18847  submmnd  18848  eqger  19218  eqgcpbl  19222  ghmqusnsglem1  19320  ghmquskerlem1  19323  gaorber  19348  orbsta  19353  cayleyth  19457  pmtrrn2  19502  pmtrfinv  19503  pmtrfmvdn0  19504  dfod2  19606  sylow2blem1  19662  sylow2blem3  19664  dprdcntz  20052  dprddisj  20053  dprdffsupp  20058  dpjdisj  20097  ablfac1a  20113  ablfac1b  20114  lmodvsdir  20906  lmhmlin  21057  lbsind  21102  2idlcpblrng  21304  mpfind  22154  mdetunilem2  22640  mdetunilem5  22643  mdetunilem6  22644  mnfnei  23250  cnprcl  23274  lmcvg  23291  lmff  23330  lmcls  23331  lmcnp  23333  fbasssin  23865  flimfil  23998  tgpconncomp  24142  tlmtrg  24219  ustssel  24235  ustincl  24237  ustdiag  24238  ustinvel  24239  ustexhalf  24240  ustfilxp  24242  tustopn  24301  tususp  24302  imasdsf1olem  24404  xmeter  24464  xmetresbl  24468  tmstopn  24519  metustexhalf  24590  nlmnrg  24721  qdensere  24811  blcvx  24839  tgqioo  24841  icccmplem1  24863  icccmplem2  24864  reconnlem1  24867  cnmpopc  24974  iccpnfcnv  24994  phtpcer  25046  phtpcco2  25051  pcohtpy  25072  pcorev2  25080  pcophtb  25081  om1addcl  25085  pi1blem  25091  pi1cpbl  25096  pi1grplem  25101  pi1inv  25104  pi1xfrf  25105  pi1xfr  25107  pi1xfrcnvlem  25108  pi1cof  25111  pi1coghm  25113  cphreccllem  25231  cphsca  25232  cphsubrg  25233  cphsqrtcl2  25239  phclm  25285  tcphcph  25290  lmmcvg  25314  cmetcaulem  25341  lmcau  25366  bcthlem3  25379  bcthlem4  25380  minveclem4c  25478  minveclem2  25479  minveclem3b  25481  minveclem4  25485  minveclem6  25487  ivthicc  25512  ovollb2lem  25542  ovolshftlem1  25563  ovolscalem1  25567  ovolicc1  25570  ovolicc2lem2  25572  ovolicc2lem3  25573  ovolicc2lem4  25574  ovolicc2lem5  25575  ioombl1lem1  25612  dyadmaxlem  25651  volivth  25661  vitalilem2  25663  vitalilem4  25665  i1fima2  25733  itg2monolem1  25805  itgcnlem  25845  itgrevallem1  25850  itgreval  25852  itgle  25865  ibladd  25876  iblabslem  25883  itgspliticc  25892  itgsplitioo  25893  ditgcl  25913  ditgswap  25914  ditgsplitlem  25915  limcdif  25931  limcresi  25940  limcres  25941  limccnp  25946  limccnp2  25947  limcun  25950  dvlip  26052  dvlip2  26054  dveq0  26059  dvgt0lem1  26061  dvivthlem1  26067  dvcnvrelem1  26076  dvcnvre  26078  dvfsumlem2  26087  dvfsumlem2OLD  26088  ftc1lem1  26096  ftc1lem2  26097  ftc1a  26098  ftc1lem4  26100  ftc2  26105  ftc2ditglem  26106  itgsubstlem  26109  ply1rem  26225  fta1glem2  26228  ig1pdvds  26239  plyrem  26365  fta1lem  26367  vieta1lem2  26371  aaliou3lem3  26404  pserulm  26483  psercnlem2  26486  psercnlem1  26487  psercn  26488  pserdvlem1  26489  pserdvlem2  26490  abelth2  26504  coseq00topi  26562  coseq0negpitopi  26563  cosordlem  26590  tanord1  26597  efif1olem1  26602  dvloglem  26708  efopnlem1  26716  logreclem  26823  relogbval  26833  nnlogbexp  26842  logbrec  26843  chordthmlem4  26896  quart1  26917  quartlem2  26919  quartlem3  26920  quart  26922  acosbnd  26961  atancj  26971  atanlogsublem  26976  atantan  26984  atanbndlem  26986  atans2  26992  dvatan  26996  atantayl  26998  divsqrtsumlem  27041  ftalem5  27138  basellem5  27146  ppisval  27165  chtleppi  27272  chpchtsum  27281  chpub  27282  mersenne  27289  perfectlem2  27292  dchrinv  27323  rplogsumlem2  27547  chpdifbndlem1  27615  pntibndlem2  27653  pntlema  27658  pntlemb  27659  pntlemg  27660  pntlemh  27661  pntlemr  27664  pntlemj  27665  pntlemf  27667  pntlemk  27668  pntlemo  27669  pntlemp  27672  pntleml  27673  abvcxp  27677  ostth2lem2  27696  scutun12  27873  slerec  27882  cofcut2  27974  cofcutr  27976  cofcutrtime  27979  cutmax  27986  cutmin  27987  addsproplem5  28024  addsproplem6  28025  sleadd1  28040  addsuniflem  28052  addsasslem1  28054  addsasslem2  28055  negsproplem4  28081  negsproplem6  28083  negscut2  28090  negsunif  28105  mulsproplem12  28171  ssltmul1  28191  ssltmul2  28192  mulsuniflem  28193  precsexlem11  28259  axtgcont1  28494  cgr3simp3  28548  legso  28625  hlln  28633  hltr  28636  btwnhl  28640  mirhl  28705  mirbtwnhl  28706  opphllem4  28776  opphl  28780  hlpasch  28782  cgracgr  28844  cgraswap  28846  cgrahl  28853  cgracol  28854  inagswap  28867  inagne3  28870  dfcgrg2  28889  umgrnloopv  29141  umgredgne  29180  usgrnloopvALT  29236  frusgrnn0  29607  cusgrm1rusgr  29618  upgrclwlkcompim  29817  2wlkdlem6  29964  2wlkond  29970  2trlond  29972  numclwwlk2lem1  30408  numclwlk2lem2f1o  30411  tncp  30510  grpolidinv  30533  nvs  30695  nvz  30701  nvtri  30702  sspn  30768  minvecolem2  30907  minvecolem4c  30911  minvecolem4  30912  minvecolem5  30913  minvecolem6  30914  adj1  31965  eliccelico  32782  elicoelioo  32783  pmtrto1cl  33092  cyc3evpm  33143  slmdvsdir  33195  slmd0vs  33203  sdrgdvcl  33266  sdrginvcl  33267  nsgqusf1olem3  33408  prmidl  33433  prmidlc  33441  qsidomlem2  33446  qsnzr  33448  mxidlmax  33458  qsdrnglem2  33489  0ringmon1p  33548  ig1pmindeg  33587  ply1degltdimlem  33635  irngss  33687  ply1annig1p  33697  minplycl  33699  algextdeglem3  33710  algextdeglem4  33711  locfinreflem  33786  cnre2csqlem  33856  sigaclci  34096  unelsiga  34098  insiga  34101  unelldsys  34122  ldsysgenld  34124  sigapildsys  34126  ldgenpisyslem1  34127  measvun  34173  cntmeas  34190  sibfima  34303  signstfveq0  34554  tg5segofs  34650  bnj1018g  34939  bnj1018  34940  pfxwlk  35091  revwlk  35092  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  36301  weiunfrlem  36430  weiunfr  36433  relowlssretop  37329  ibladdnc  37637  iblabsnclem  37643  ftc2nc  37662  dvasin  37664  isbndx  37742  isbnd3  37744  prdsbnd  37753  heiborlem3  37773  iccbnd  37800  rngohomadd  37929  rngohommul  37930  idladdcl  37979  idllmulcl  37980  idlrmulcl  37981  maxidlmax  38003  pridlc  38031  eqvreltr  38563  lshpnelb  38940  lshpcmp  38944  oplecon3  39155  opnoncon  39164  hlcvl  39315  dochshpncl  41341  lclkrslem1  41494  lclkrslem2  41495  fzne2d  41937  primrootsunit1  42054  primrootscoprmpow  42056  primrootlekpowne0  42062  aks6d1c1p1  42064  aks6d1c2  42087  sticksstones3  42105  aks5lem1  42143  aks5lem2  42144  aks5lem3a  42146  metakunt8  42169  metakunt20  42181  metakunt21  42182  metakunt22  42183  metakunt24  42185  metakunt25  42186  evlsval3  42514  flt4lem5f  42612  flt4lem7  42614  nna4b4nsq  42615  acongrep  42937  ntrneinex  44039  neicvgmex  44079  gneispace0nelrn  44102  cvgdvgrat  44282  binomcxplemdvbinom  44322  eliocre  45427  iccshift  45436  iccsuble  45437  icoiccdif  45442  mullimc  45537  limccog  45541  limciccioolb  45542  mullimcf  45544  limcperiod  45549  lptioo2  45552  lptioo1  45553  neglimc  45568  addlimc  45569  0ellimcdiv  45570  reclimc  45574  xlimmnfvlem1  45753  xlimpnfvlem1  45757  icccncfext  45808  cncfioobdlem  45817  ditgeqiooicc  45881  iblspltprt  45894  iblcncfioo  45899  itgiccshift  45901  itgperiod  45902  itgsbtaddcnst  45903  stoweidlem11  45932  stoweidlem31  45952  stoweidlem36  45957  stoweidlem38  45959  stoweidlem62  45983  dirkercncflem1  46024  dirkercncflem4  46027  fourierdlem26  46054  fourierdlem32  46060  fourierdlem33  46061  fourierdlem37  46065  fourierdlem42  46070  fourierdlem54  46081  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem74  46101  fourierdlem75  46102  fourierdlem79  46106  fourierdlem81  46108  fourierdlem82  46109  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem93  46120  fourierdlem101  46128  fourierdlem107  46134  fourierdlem109  46136  fourierdlem111  46138  salunicl  46237  saluncl  46238  hoidmv1lelem1  46512  hoidmv1lelem3  46514  hoidmvlelem1  46516  ovolval3  46568  iinhoiicclem  46594  smfpreimalt  46652  smfpreimaltf  46657  smfpreimale  46675  issmfgt  46677  smfpreimagt  46683  smfpreimage  46703  sigardiv  46782  sigarcol  46785  sharhght  46786  sigaradd  46787  cevathlem1  46788  cevathlem2  46789  cevath  46790  proththd  47488  perfectALTVlem2  47596