Theorem simp3d 1162

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 1156	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp3bi  1165  f1dom3fv3dif  7269  f1dom3el3dif  7270  oeeui  8594  resixp  8944  domssex2  9139  cantnflem1c  9670  cantnflem1  9672  cantnflem3  9674  cantnflem4  9675  fpwwe2lem6  10649  canthnumlem  10661  canthp1lem2  10666  wununi  10719  wunpw  10720  wunpr  10722  lelttrdi  11400  ixxdisj  13417  ixxun  13418  ixxss1  13420  ixxss2  13421  ixxss12  13422  ixxub  13423  ixxlb  13424  lbioo  13433  elicore  13455  iccsupr  13499  icodisj  13533  xov1plusxeqvd  13555  intfracq  13924  fldiv  13925  seqf1olem2  14110  cjmul  15233  icco1  15631  sumtp  15839  rpnnen2lem10  16317  ruclem2  16326  ruclem3  16327  ruclem9  16332  ruclem12  16335  dvdslegcd  16600  prmdvdsbc  16823  crth  16875  eulerthlem1  16878  eulerthlem2  16879  pcpremul  16941  prmreclem2  17015  prmreclem3  17016  4sqlem13  17055  sectcan  17850  sectco  17851  sectmon  17877  monsect  17878  funcid  17965  funcco  17966  funcsect  17967  invfuc  18072  fuciso  18073  coapm  18166  catciso  18206  postr  18414  ipodrsima  18635  psref2  18664  psasym  18670  mhm0  18908  submcl  18926  submmnd  18928  eqger  19309  eqgcpbl  19313  ghmqusnsglem1  19413  ghmquskerlem1  19416  gaorber  19441  orbsta  19446  cayleyth  19548  pmtrrn2  19593  pmtrfinv  19594  pmtrfmvdn0  19595  dfod2  19697  sylow2blem1  19753  sylow2blem3  19755  dprdcntz  20143  dprddisj  20144  dprdffsupp  20149  dpjdisj  20188  ablfac1a  20204  ablfac1b  20205  lmodvsdir  21076  lmhmlin  21225  lbsind  21270  2idlcpblrng  21479  prmidl  21534  prmidlc  21542  prmidlprop  21545  qsidomlem2  21550  qsnzr  21552  evlsval3  22311  mpfind  22337  mdetunilem2  22841  mdetunilem5  22844  mdetunilem6  22845  mnfnei  23452  cnprcl  23476  lmcvg  23493  lmff  23532  lmcls  23533  lmcnp  23535  fbasssin  24068  flimfil  24201  tgpconncomp  24345  tlmtrg  24422  ustssel  24438  ustincl  24440  ustdiag  24441  ustinvel  24442  ustexhalf  24443  ustfilxp  24445  tustopn  24502  tususp  24503  imasdsf1olem  24605  xmeter  24665  xmetresbl  24669  tmstopn  24717  metustexhalf  24788  nlmnrg  24911  qdensere  25001  blcvx  25030  tgqioo  25032  icccmplem1  25055  icccmplem2  25056  reconnlem1  25059  cnmpopc  25162  iccpnfcnv  25178  phtpcer  25229  phtpcco2  25233  pcohtpy  25254  pcorev2  25262  pcophtb  25263  om1addcl  25267  pi1blem  25273  pi1cpbl  25278  pi1grplem  25283  pi1inv  25286  pi1xfrf  25287  pi1xfr  25289  pi1xfrcnvlem  25290  pi1cof  25293  pi1coghm  25295  cphreccllem  25412  cphsca  25413  cphsubrg  25414  cphsqrtcl2  25420  phclm  25466  tcphcph  25471  lmmcvg  25495  cmetcaulem  25522  lmcau  25547  bcthlem3  25560  bcthlem4  25561  minveclem4c  25659  minveclem2  25660  minveclem3b  25662  minveclem4  25666  minveclem6  25668  ivthicc  25692  ovollb2lem  25722  ovolshftlem1  25743  ovolscalem1  25747  ovolicc1  25750  ovolicc2lem2  25752  ovolicc2lem3  25753  ovolicc2lem4  25754  ovolicc2lem5  25755  ioombl1lem1  25792  dyadmaxlem  25831  volivth  25841  vitalilem2  25843  vitalilem4  25845  i1fima2  25913  itg2monolem1  25984  itgcnlem  26024  itgrevallem1  26029  itgreval  26031  itgle  26044  ibladd  26055  iblabslem  26062  itgspliticc  26071  itgsplitioo  26072  ditgcl  26092  ditgswap  26093  ditgsplitlem  26094  limcdif  26110  limcresi  26119  limcres  26120  limccnp  26125  limccnp2  26126  limcun  26129  dvlip  26227  dvlip2  26229  dveq0  26234  dvgt0lem1  26236  dvivthlem1  26242  dvcnvrelem1  26251  dvcnvre  26253  dvfsumlem2  26261  ftc1lem1  26269  ftc1lem2  26270  ftc1a  26271  ftc1lem4  26273  ftc2  26278  ftc2ditglem  26279  itgsubstlem  26282  ply1rem  26398  fta1glem2  26401  ig1pdvds  26412  plyrem  26542  fta1lem  26544  vieta1lem2  26550  aaliou3lem3  26587  pserulm  26665  psercnlem2  26667  psercnlem1  26668  psercn  26669  pserdvlem1  26670  pserdvlem2  26671  abelth2  26685  coseq00topi  26747  coseq0negpitopi  26748  cosordlem  26775  tanord1  26782  efif1olem1  26787  dvloglem  26893  efopnlem1  26901  logreclem  27007  relogbval  27017  nnlogbexp  27026  logbrec  27027  chordthmlem4  27080  quart1  27101  quartlem2  27103  quartlem3  27104  quart  27106  acosbnd  27145  atancj  27155  atanlogsublem  27160  atantan  27168  atanbndlem  27170  atans2  27176  dvatan  27180  atantayl  27182  divsqrtsumlem  27224  ftalem5  27321  basellem5  27329  ppisval  27348  chtleppi  27454  chpchtsum  27463  chpub  27464  mersenne  27471  perfectlem2  27474  dchrinv  27505  rplogsumlem2  27729  chpdifbndlem1  27797  pntibndlem2  27835  pntlema  27840  pntlemb  27841  pntlemg  27842  pntlemh  27843  pntlemr  27846  pntlemj  27847  pntlemf  27849  pntlemk  27850  pntlemo  27851  pntlemp  27854  pntleml  27855  abvcxp  27859  ostth2lem2  27878  cutsun12  28063  lesrec  28072  eqcuts3  28077  cofcut2  28195  cofcutr  28197  cofcutrtime  28200  cutmax  28207  cutmin  28208  addsproplem5  28246  addsproplem6  28247  leadds1  28262  addsuniflem  28274  addsasslem1  28276  addsasslem2  28277  negsproplem4  28304  negsproplem6  28306  negcut2  28313  negsunif  28328  mulsproplem12  28400  sltmuls1  28420  sltmuls2  28421  mulsuniflem  28422  precsexlem11  28490  twocut  28696  pw2cut2  28735  axtgcont1  28817  cgr3simp3  28872  legso  28949  hlln  28960  hltr  28963  btwnhl  28967  tghlsub  28973  mirhl  29038  mirbtwnhl  29039  opphllem4  29113  opphl  29117  hlpasch  29121  cgracgr  29212  cgraswap  29214  cgrahl  29222  cgracol  29223  inagswap  29247  inagne3  29250  dfcgrg2  29295  umgrnloopv  29571  umgredgne  29610  usgrnloopvALT  29669  frusgrnn0  30039  cusgrm1rusgr  30050  pfxwlk  30153  revwlk  30154  upgrclwlkcompim  30255  spthcycl  30279  2wlkdlem6  30407  2wlkond  30413  2trlond  30415  acycgrcycl  30640  numclwwlk2lem1  30864  numclwlk2lem2f1o  30867  tncp  30967  grpolidinv  30990  nvs  31152  nvz  31158  nvtri  31159  sspn  31225  minvecolem2  31364  minvecolem4c  31368  minvecolem4  31369  minvecolem5  31370  minvecolem6  31371  adj1  32422  eliccelico  33256  elicoelioo  33257  pmtrto1cl  33547  cyc3evpm  33598  slmdvsdir  33664  slmd0vs  33672  sdrgdvcl  33748  sdrginvcl  33749  nsgqusf1olem3  33852  mxidlmax  33876  qsdrnglem2  33906  0ringmon1p  33975  ig1pmindeg  34020  ply1degltdimlem  34140  irngss  34205  ply1annig1p  34222  minplycl  34224  algextdeglem3  34237  algextdeglem4  34238  constrsqrtcl  34297  locfinreflem  34358  cnre2csqlem  34428  sigaclci  34650  unelsiga  34652  insiga  34656  unelldsys  34677  ldsysgenld  34679  sigapildsys  34681  ldgenpisyslem1  34682  measvun  34728  cntmeas  34745  sibfima  34857  signstfveq0  35093  cgranbtwn  35185  tg5segofs  35192  bnj1018g  35480  bnj1018  35481  subfacp1lem3  35769  subfacp1lem4  35770  subfacp1lem5  35771  sconnpht2  35825  sconnpi1  35826  txsconn  35828  resconn  35833  cvmcn  35849  cvmsuni  35856  cvmsdisj  35857  cvmshmeo  35858  cvmlift2lem8  35897  cvmlift2lem13  35902  cvmliftphtlem  35904  cvmliftpht  35905  cvmlift3lem6  35911  msrf  36129  elmsta  36135  mthmpps  36169  mclsppslem  36170  ivthALT  36962  weiunfrlem  37091  weiunfr  37094  relowlssretop  38125  ibladdnc  38434  iblabsnclem  38440  ftc2nc  38459  dvasin  38461  isbndx  38540  isbnd3  38542  prdsbnd  38551  heiborlem3  38571  iccbnd  38598  rngohomadd  38727  rngohommul  38728  idladdcl  38777  idllmulcl  38778  idlrmulcl  38779  maxidlmax  38801  pridlc  38829  eqvreltr  39447  lshpnelb  39865  lshpcmp  39869  oplecon3  40080  opnoncon  40089  hlcvl  40240  dochshpncl  42265  lclkrslem1  42418  lclkrslem2  42419  fzne2d  42854  primrootsunit1  42971  primrootscoprmpow  42973  primrootlekpowne0  42979  aks6d1c1p1  42981  aks6d1c2  43004  sticksstones3  43022  aks5lem1  43060  aks5lem2  43061  aks5lem3a  43063  flt4lem5f  43511  flt4lem7  43513  nna4b4nsq  43514  acongrep  43829  ntrneinex  44925  neicvgmex  44965  gneispace0nelrn  44988  cvgdvgrat  45145  binomcxplemdvbinom  45185  eliocre  46347  iccshift  46356  iccsuble  46357  icoiccdif  46362  mullimc  46454  limccog  46458  limciccioolb  46459  mullimcf  46461  limcperiod  46466  lptioo2  46469  lptioo1  46470  neglimc  46483  addlimc  46484  0ellimcdiv  46485  reclimc  46489  xlimmnfvlem1  46668  xlimpnfvlem1  46672  icccncfext  46723  cncfioobdlem  46732  ditgeqiooicc  46796  iblspltprt  46809  iblcncfioo  46814  itgiccshift  46816  itgperiod  46817  itgsbtaddcnst  46818  stoweidlem11  46847  stoweidlem31  46867  stoweidlem36  46872  stoweidlem38  46874  stoweidlem62  46898  dirkercncflem1  46939  dirkercncflem4  46942  fourierdlem26  46969  fourierdlem32  46975  fourierdlem33  46976  fourierdlem37  46980  fourierdlem42  46985  fourierdlem54  46996  fourierdlem63  47005  fourierdlem64  47006  fourierdlem65  47007  fourierdlem74  47016  fourierdlem75  47017  fourierdlem79  47021  fourierdlem81  47023  fourierdlem82  47024  fourierdlem89  47031  fourierdlem90  47032  fourierdlem91  47033  fourierdlem93  47035  fourierdlem101  47043  fourierdlem107  47049  fourierdlem109  47051  fourierdlem111  47053  salunicl  47152  saluncl  47153  hoidmv1lelem1  47427  hoidmv1lelem3  47429  hoidmvlelem1  47431  ovolval3  47483  iinhoiicclem  47509  smfpreimalt  47567  smfpreimaltf  47572  smfpreimale  47590  issmfgt  47592  smfpreimagt  47598  smfpreimage  47618  sigardiv  47697  sigarcol  47700  sharhght  47701  sigaradd  47702  cevathlem1  47703  cevathlem2  47704  cevath  47705  proththd  48525  perfectALTVlem2  48646  gpgnbgrvtx0  48998  gpgnbgrvtx1  48999  imasubc2  50086  imaf1co  50089  idfullsubc  50095  fucofulem1  50244  rr3fv3cld  50790