Theorem simp3d 1145

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 1139	. 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  1148  f1dom3fv3dif  7216  f1dom3el3dif  7217  oeeui  8532  resixp  8875  domssex2  9069  cantnflem1c  9600  cantnflem1  9602  cantnflem3  9604  cantnflem4  9605  fpwwe2lem6  10551  canthnumlem  10563  canthp1lem2  10568  wununi  10621  wunpw  10622  wunpr  10624  lelttrdi  11299  ixxdisj  13280  ixxun  13281  ixxss1  13283  ixxss2  13284  ixxss12  13285  ixxub  13286  ixxlb  13287  lbioo  13296  elicore  13318  iccsupr  13362  icodisj  13396  xov1plusxeqvd  13418  intfracq  13783  fldiv  13784  seqf1olem2  13969  cjmul  15069  icco1  15467  sumtp  15676  rpnnen2lem10  16152  ruclem2  16161  ruclem3  16162  ruclem9  16167  ruclem12  16170  dvdslegcd  16435  prmdvdsbc  16657  crth  16709  eulerthlem1  16712  eulerthlem2  16713  pcpremul  16775  prmreclem2  16849  prmreclem3  16850  4sqlem13  16889  sectcan  17683  sectco  17684  sectmon  17710  monsect  17711  funcid  17798  funcco  17799  funcsect  17800  invfuc  17905  fuciso  17906  coapm  17999  catciso  18039  postr  18247  ipodrsima  18468  psref2  18497  psasym  18503  mhm0  18723  submcl  18741  submmnd  18742  eqger  19111  eqgcpbl  19115  ghmqusnsglem1  19213  ghmquskerlem1  19216  gaorber  19241  orbsta  19246  cayleyth  19348  pmtrrn2  19393  pmtrfinv  19394  pmtrfmvdn0  19395  dfod2  19497  sylow2blem1  19553  sylow2blem3  19555  dprdcntz  19943  dprddisj  19944  dprdffsupp  19949  dpjdisj  19988  ablfac1a  20004  ablfac1b  20005  lmodvsdir  20841  lmhmlin  20991  lbsind  21036  2idlcpblrng  21230  evlsval3  22048  mpfind  22074  mdetunilem2  22561  mdetunilem5  22564  mdetunilem6  22565  mnfnei  23169  cnprcl  23193  lmcvg  23210  lmff  23249  lmcls  23250  lmcnp  23252  fbasssin  23784  flimfil  23917  tgpconncomp  24061  tlmtrg  24138  ustssel  24154  ustincl  24156  ustdiag  24157  ustinvel  24158  ustexhalf  24159  ustfilxp  24161  tustopn  24218  tususp  24219  imasdsf1olem  24321  xmeter  24381  xmetresbl  24385  tmstopn  24433  metustexhalf  24504  nlmnrg  24627  qdensere  24717  blcvx  24746  tgqioo  24748  icccmplem1  24771  icccmplem2  24772  reconnlem1  24775  cnmpopc  24882  iccpnfcnv  24902  phtpcer  24954  phtpcco2  24959  pcohtpy  24980  pcorev2  24988  pcophtb  24989  om1addcl  24993  pi1blem  24999  pi1cpbl  25004  pi1grplem  25009  pi1inv  25012  pi1xfrf  25013  pi1xfr  25015  pi1xfrcnvlem  25016  pi1cof  25019  pi1coghm  25021  cphreccllem  25138  cphsca  25139  cphsubrg  25140  cphsqrtcl2  25146  phclm  25192  tcphcph  25197  lmmcvg  25221  cmetcaulem  25248  lmcau  25273  bcthlem3  25286  bcthlem4  25287  minveclem4c  25385  minveclem2  25386  minveclem3b  25388  minveclem4  25392  minveclem6  25394  ivthicc  25419  ovollb2lem  25449  ovolshftlem1  25470  ovolscalem1  25474  ovolicc1  25477  ovolicc2lem2  25479  ovolicc2lem3  25480  ovolicc2lem4  25481  ovolicc2lem5  25482  ioombl1lem1  25519  dyadmaxlem  25558  volivth  25568  vitalilem2  25570  vitalilem4  25572  i1fima2  25640  itg2monolem1  25711  itgcnlem  25751  itgrevallem1  25756  itgreval  25758  itgle  25771  ibladd  25782  iblabslem  25789  itgspliticc  25798  itgsplitioo  25799  ditgcl  25819  ditgswap  25820  ditgsplitlem  25821  limcdif  25837  limcresi  25846  limcres  25847  limccnp  25852  limccnp2  25853  limcun  25856  dvlip  25958  dvlip2  25960  dveq0  25965  dvgt0lem1  25967  dvivthlem1  25973  dvcnvrelem1  25982  dvcnvre  25984  dvfsumlem2  25993  dvfsumlem2OLD  25994  ftc1lem1  26002  ftc1lem2  26003  ftc1a  26004  ftc1lem4  26006  ftc2  26011  ftc2ditglem  26012  itgsubstlem  26015  ply1rem  26131  fta1glem2  26134  ig1pdvds  26145  plyrem  26273  fta1lem  26275  vieta1lem2  26279  aaliou3lem3  26312  pserulm  26391  psercnlem2  26394  psercnlem1  26395  psercn  26396  pserdvlem1  26397  pserdvlem2  26398  abelth2  26412  coseq00topi  26471  coseq0negpitopi  26472  cosordlem  26499  tanord1  26506  efif1olem1  26511  dvloglem  26617  efopnlem1  26625  logreclem  26732  relogbval  26742  nnlogbexp  26751  logbrec  26752  chordthmlem4  26805  quart1  26826  quartlem2  26828  quartlem3  26829  quart  26831  acosbnd  26870  atancj  26880  atanlogsublem  26885  atantan  26893  atanbndlem  26895  atans2  26901  dvatan  26905  atantayl  26907  divsqrtsumlem  26950  ftalem5  27047  basellem5  27055  ppisval  27074  chtleppi  27181  chpchtsum  27190  chpub  27191  mersenne  27198  perfectlem2  27201  dchrinv  27232  rplogsumlem2  27456  chpdifbndlem1  27524  pntibndlem2  27562  pntlema  27567  pntlemb  27568  pntlemg  27569  pntlemh  27570  pntlemr  27573  pntlemj  27574  pntlemf  27576  pntlemk  27577  pntlemo  27578  pntlemp  27581  pntleml  27582  abvcxp  27586  ostth2lem2  27605  scutun12  27788  slerec  27797  eqscut3  27802  cofcut2  27904  cofcutr  27906  cofcutrtime  27909  cutmax  27916  cutmin  27917  addsproplem5  27955  addsproplem6  27956  sleadd1  27971  addsuniflem  27983  addsasslem1  27985  addsasslem2  27986  negsproplem4  28013  negsproplem6  28015  negscut2  28022  negsunif  28037  mulsproplem12  28109  ssltmul1  28129  ssltmul2  28130  mulsuniflem  28131  precsexlem11  28198  twocut  28402  pw2cut2  28441  axtgcont1  28523  cgr3simp3  28577  legso  28654  hlln  28662  hltr  28665  btwnhl  28669  mirhl  28734  mirbtwnhl  28735  opphllem4  28805  opphl  28809  hlpasch  28811  cgracgr  28873  cgraswap  28875  cgrahl  28882  cgracol  28883  inagswap  28896  inagne3  28899  dfcgrg2  28918  umgrnloopv  29162  umgredgne  29201  usgrnloopvALT  29257  frusgrnn0  29628  cusgrm1rusgr  29639  upgrclwlkcompim  29837  2wlkdlem6  29987  2wlkond  29993  2trlond  29995  numclwwlk2lem1  30434  numclwlk2lem2f1o  30437  tncp  30536  grpolidinv  30559  nvs  30721  nvz  30727  nvtri  30728  sspn  30794  minvecolem2  30933  minvecolem4c  30937  minvecolem4  30938  minvecolem5  30939  minvecolem6  30940  adj1  31991  eliccelico  32838  elicoelioo  32839  pmtrto1cl  33162  cyc3evpm  33213  slmdvsdir  33279  slmd0vs  33287  sdrgdvcl  33362  sdrginvcl  33363  nsgqusf1olem3  33477  prmidl  33502  prmidlc  33510  qsidomlem2  33515  qsnzr  33517  mxidlmax  33527  qsdrnglem2  33558  0ringmon1p  33619  ig1pmindeg  33664  ply1degltdimlem  33760  irngss  33825  ply1annig1p  33842  minplycl  33844  algextdeglem3  33857  algextdeglem4  33858  constrsqrtcl  33917  locfinreflem  33978  cnre2csqlem  34048  sigaclci  34270  unelsiga  34272  insiga  34275  unelldsys  34296  ldsysgenld  34298  sigapildsys  34300  ldgenpisyslem1  34301  measvun  34347  cntmeas  34364  sibfima  34476  signstfveq0  34715  tg5segofs  34811  bnj1018g  35100  bnj1018  35101  pfxwlk  35299  revwlk  35300  spthcycl  35304  acycgrcycl  35322  subfacp1lem3  35357  subfacp1lem4  35358  subfacp1lem5  35359  sconnpht2  35413  sconnpi1  35414  txsconn  35416  resconn  35421  cvmcn  35437  cvmsuni  35444  cvmsdisj  35445  cvmshmeo  35446  cvmlift2lem8  35485  cvmlift2lem13  35490  cvmliftphtlem  35492  cvmliftpht  35493  cvmlift3lem6  35499  msrf  35717  elmsta  35723  mthmpps  35757  mclsppslem  35758  ivthALT  36510  weiunfrlem  36639  weiunfr  36642  relowlssretop  37539  ibladdnc  37849  iblabsnclem  37855  ftc2nc  37874  dvasin  37876  isbndx  37954  isbnd3  37956  prdsbnd  37965  heiborlem3  37985  iccbnd  38012  rngohomadd  38141  rngohommul  38142  idladdcl  38191  idllmulcl  38192  idlrmulcl  38193  maxidlmax  38215  pridlc  38243  eqvreltr  38863  lshpnelb  39281  lshpcmp  39285  oplecon3  39496  opnoncon  39505  hlcvl  39656  dochshpncl  41681  lclkrslem1  41834  lclkrslem2  41835  fzne2d  42271  primrootsunit1  42388  primrootscoprmpow  42390  primrootlekpowne0  42396  aks6d1c1p1  42398  aks6d1c2  42421  sticksstones3  42439  aks5lem1  42477  aks5lem2  42478  aks5lem3a  42480  flt4lem5f  42936  flt4lem7  42938  nna4b4nsq  42939  acongrep  43258  ntrneinex  44354  neicvgmex  44394  gneispace0nelrn  44417  cvgdvgrat  44590  binomcxplemdvbinom  44630  eliocre  45791  iccshift  45800  iccsuble  45801  icoiccdif  45806  mullimc  45898  limccog  45902  limciccioolb  45903  mullimcf  45905  limcperiod  45910  lptioo2  45913  lptioo1  45914  neglimc  45927  addlimc  45928  0ellimcdiv  45929  reclimc  45933  xlimmnfvlem1  46112  xlimpnfvlem1  46116  icccncfext  46167  cncfioobdlem  46176  ditgeqiooicc  46240  iblspltprt  46253  iblcncfioo  46258  itgiccshift  46260  itgperiod  46261  itgsbtaddcnst  46262  stoweidlem11  46291  stoweidlem31  46311  stoweidlem36  46316  stoweidlem38  46318  stoweidlem62  46342  dirkercncflem1  46383  dirkercncflem4  46386  fourierdlem26  46413  fourierdlem32  46419  fourierdlem33  46420  fourierdlem37  46424  fourierdlem42  46429  fourierdlem54  46440  fourierdlem63  46449  fourierdlem64  46450  fourierdlem65  46451  fourierdlem74  46460  fourierdlem75  46461  fourierdlem79  46465  fourierdlem81  46467  fourierdlem82  46468  fourierdlem89  46475  fourierdlem90  46476  fourierdlem91  46477  fourierdlem93  46479  fourierdlem101  46487  fourierdlem107  46493  fourierdlem109  46495  fourierdlem111  46497  salunicl  46596  saluncl  46597  hoidmv1lelem1  46871  hoidmv1lelem3  46873  hoidmvlelem1  46875  ovolval3  46927  iinhoiicclem  46953  smfpreimalt  47011  smfpreimaltf  47016  smfpreimale  47034  issmfgt  47036  smfpreimagt  47042  smfpreimage  47062  sigardiv  47141  sigarcol  47144  sharhght  47145  sigaradd  47146  cevathlem1  47147  cevathlem2  47148  cevath  47149  proththd  47896  perfectALTVlem2  48004  gpgnbgrvtx0  48356  gpgnbgrvtx1  48357  imasubc2  49433  imaf1co  49436  idfullsubc  49442  fucofulem1  49591