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  7273  f1dom3el3dif  7274  oeeui  8597  resixp  8940  domssex2  9135  cantnflem1c  9666  cantnflem1  9668  cantnflem3  9670  cantnflem4  9671  fpwwe2lem6  10639  canthnumlem  10651  canthp1lem2  10656  wununi  10709  wunpw  10710  wunpr  10712  lelttrdi  11390  ixxdisj  13405  ixxun  13406  ixxss1  13408  ixxss2  13409  ixxss12  13410  ixxub  13411  ixxlb  13412  lbioo  13421  elicore  13443  iccsupr  13487  icodisj  13521  xov1plusxeqvd  13543  intfracq  13912  fldiv  13913  seqf1olem2  14098  cjmul  15219  icco1  15617  sumtp  15826  rpnnen2lem10  16304  ruclem2  16313  ruclem3  16314  ruclem9  16319  ruclem12  16322  dvdslegcd  16587  prmdvdsbc  16810  crth  16862  eulerthlem1  16865  eulerthlem2  16866  pcpremul  16928  prmreclem2  17002  prmreclem3  17003  4sqlem13  17042  sectcan  17837  sectco  17838  sectmon  17864  monsect  17865  funcid  17952  funcco  17953  funcsect  17954  invfuc  18059  fuciso  18060  coapm  18153  catciso  18193  postr  18401  ipodrsima  18622  psref2  18651  psasym  18657  mhm0  18877  submcl  18895  submmnd  18897  eqger  19271  eqgcpbl  19275  ghmqusnsglem1  19375  ghmquskerlem1  19378  gaorber  19403  orbsta  19408  cayleyth  19510  pmtrrn2  19555  pmtrfinv  19556  pmtrfmvdn0  19557  dfod2  19659  sylow2blem1  19715  sylow2blem3  19717  dprdcntz  20105  dprddisj  20106  dprdffsupp  20111  dpjdisj  20150  ablfac1a  20166  ablfac1b  20167  lmodvsdir  21037  lmhmlin  21186  lbsind  21231  2idlcpblrng  21440  prmidl  21495  prmidlc  21503  prmidlprop  21506  qsidomlem2  21511  qsnzr  21513  evlsval3  22270  mpfind  22296  mdetunilem2  22800  mdetunilem5  22803  mdetunilem6  22804  mnfnei  23408  cnprcl  23432  lmcvg  23449  lmff  23488  lmcls  23489  lmcnp  23491  fbasssin  24023  flimfil  24156  tgpconncomp  24300  tlmtrg  24377  ustssel  24393  ustincl  24395  ustdiag  24396  ustinvel  24397  ustexhalf  24398  ustfilxp  24400  tustopn  24457  tususp  24458  imasdsf1olem  24560  xmeter  24620  xmetresbl  24624  tmstopn  24672  metustexhalf  24743  nlmnrg  24866  qdensere  24956  blcvx  24985  tgqioo  24987  icccmplem1  25010  icccmplem2  25011  reconnlem1  25014  cnmpopc  25117  iccpnfcnv  25133  phtpcer  25184  phtpcco2  25188  pcohtpy  25209  pcorev2  25217  pcophtb  25218  om1addcl  25222  pi1blem  25228  pi1cpbl  25233  pi1grplem  25238  pi1inv  25241  pi1xfrf  25242  pi1xfr  25244  pi1xfrcnvlem  25245  pi1cof  25248  pi1coghm  25250  cphreccllem  25367  cphsca  25368  cphsubrg  25369  cphsqrtcl2  25375  phclm  25421  tcphcph  25426  lmmcvg  25450  cmetcaulem  25477  lmcau  25502  bcthlem3  25515  bcthlem4  25516  minveclem4c  25614  minveclem2  25615  minveclem3b  25617  minveclem4  25621  minveclem6  25623  ivthicc  25647  ovollb2lem  25677  ovolshftlem1  25698  ovolscalem1  25702  ovolicc1  25705  ovolicc2lem2  25707  ovolicc2lem3  25708  ovolicc2lem4  25709  ovolicc2lem5  25710  ioombl1lem1  25747  dyadmaxlem  25786  volivth  25796  vitalilem2  25798  vitalilem4  25800  i1fima2  25868  itg2monolem1  25939  itgcnlem  25979  itgrevallem1  25984  itgreval  25986  itgle  25999  ibladd  26010  iblabslem  26017  itgspliticc  26026  itgsplitioo  26027  ditgcl  26047  ditgswap  26048  ditgsplitlem  26049  limcdif  26065  limcresi  26074  limcres  26075  limccnp  26080  limccnp2  26081  limcun  26084  dvlip  26182  dvlip2  26184  dveq0  26189  dvgt0lem1  26191  dvivthlem1  26197  dvcnvrelem1  26206  dvcnvre  26208  dvfsumlem2  26216  ftc1lem1  26224  ftc1lem2  26225  ftc1a  26226  ftc1lem4  26228  ftc2  26233  ftc2ditglem  26234  itgsubstlem  26237  ply1rem  26353  fta1glem2  26356  ig1pdvds  26367  plyrem  26496  fta1lem  26498  vieta1lem2  26502  aaliou3lem3  26537  pserulm  26615  psercnlem2  26617  psercnlem1  26618  psercn  26619  pserdvlem1  26620  pserdvlem2  26621  abelth2  26635  coseq00topi  26697  coseq0negpitopi  26698  cosordlem  26725  tanord1  26732  efif1olem1  26737  dvloglem  26843  efopnlem1  26851  logreclem  26957  relogbval  26967  nnlogbexp  26976  logbrec  26977  chordthmlem4  27030  quart1  27051  quartlem2  27053  quartlem3  27054  quart  27056  acosbnd  27095  atancj  27105  atanlogsublem  27110  atantan  27118  atanbndlem  27120  atans2  27126  dvatan  27130  atantayl  27132  divsqrtsumlem  27174  ftalem5  27271  basellem5  27279  ppisval  27298  chtleppi  27404  chpchtsum  27413  chpub  27414  mersenne  27421  perfectlem2  27424  dchrinv  27455  rplogsumlem2  27679  chpdifbndlem1  27747  pntibndlem2  27785  pntlema  27790  pntlemb  27791  pntlemg  27792  pntlemh  27793  pntlemr  27796  pntlemj  27797  pntlemf  27799  pntlemk  27800  pntlemo  27801  pntlemp  27804  pntleml  27805  abvcxp  27809  ostth2lem2  27828  cutsun12  28013  lesrec  28022  eqcuts3  28027  cofcut2  28145  cofcutr  28147  cofcutrtime  28150  cutmax  28157  cutmin  28158  addsproplem5  28196  addsproplem6  28197  leadds1  28212  addsuniflem  28224  addsasslem1  28226  addsasslem2  28227  negsproplem4  28254  negsproplem6  28256  negcut2  28263  negsunif  28278  mulsproplem12  28350  sltmuls1  28370  sltmuls2  28371  mulsuniflem  28372  precsexlem11  28440  twocut  28646  pw2cut2  28685  axtgcont1  28767  cgr3simp3  28821  legso  28898  hlln  28909  hltr  28912  btwnhl  28916  mirhl  28986  mirbtwnhl  28987  opphllem4  29061  opphl  29065  hlpasch  29068  cgracgr  29159  cgraswap  29161  cgrahl  29168  cgracol  29169  inagswap  29188  inagne3  29191  dfcgrg2  29210  umgrnloopv  29486  umgredgne  29525  usgrnloopvALT  29581  frusgrnn0  29951  cusgrm1rusgr  29962  upgrclwlkcompim  30160  2wlkdlem6  30310  2wlkond  30316  2trlond  30318  numclwwlk2lem1  30757  numclwlk2lem2f1o  30760  tncp  30860  grpolidinv  30883  nvs  31045  nvz  31051  nvtri  31052  sspn  31118  minvecolem2  31257  minvecolem4c  31261  minvecolem4  31262  minvecolem5  31263  minvecolem6  31264  adj1  32315  eliccelico  33152  elicoelioo  33153  pmtrto1cl  33443  cyc3evpm  33494  slmdvsdir  33560  slmd0vs  33568  sdrgdvcl  33644  sdrginvcl  33645  nsgqusf1olem3  33748  mxidlmax  33772  qsdrnglem2  33802  0ringmon1p  33871  ig1pmindeg  33916  ply1degltdimlem  34036  irngss  34101  ply1annig1p  34118  minplycl  34120  algextdeglem3  34133  algextdeglem4  34134  constrsqrtcl  34193  locfinreflem  34254  cnre2csqlem  34324  sigaclci  34546  unelsiga  34548  insiga  34551  unelldsys  34572  ldsysgenld  34574  sigapildsys  34576  ldgenpisyslem1  34577  measvun  34623  cntmeas  34640  sibfima  34752  signstfveq0  34988  cgranbtwn  35080  tg5segofs  35087  bnj1018g  35375  bnj1018  35376  pfxwlk  35629  revwlk  35630  spthcycl  35634  acycgrcycl  35652  subfacp1lem3  35687  subfacp1lem4  35688  subfacp1lem5  35689  sconnpht2  35743  sconnpi1  35744  txsconn  35746  resconn  35751  cvmcn  35767  cvmsuni  35774  cvmsdisj  35775  cvmshmeo  35776  cvmlift2lem8  35815  cvmlift2lem13  35820  cvmliftphtlem  35822  cvmliftpht  35823  cvmlift3lem6  35829  msrf  36047  elmsta  36053  mthmpps  36087  mclsppslem  36088  ivthALT  36879  weiunfrlem  37008  weiunfr  37011  relowlssretop  38042  ibladdnc  38361  iblabsnclem  38367  ftc2nc  38386  dvasin  38388  isbndx  38466  isbnd3  38468  prdsbnd  38477  heiborlem3  38497  iccbnd  38524  rngohomadd  38653  rngohommul  38654  idladdcl  38703  idllmulcl  38704  idlrmulcl  38705  maxidlmax  38727  pridlc  38755  eqvreltr  39373  lshpnelb  39791  lshpcmp  39795  oplecon3  40006  opnoncon  40015  hlcvl  40166  dochshpncl  42191  lclkrslem1  42344  lclkrslem2  42345  fzne2d  42780  primrootsunit1  42897  primrootscoprmpow  42899  primrootlekpowne0  42905  aks6d1c1p1  42907  aks6d1c2  42930  sticksstones3  42948  aks5lem1  42986  aks5lem2  42987  aks5lem3a  42989  flt4lem5f  43422  flt4lem7  43424  nna4b4nsq  43425  acongrep  43740  ntrneinex  44836  neicvgmex  44876  gneispace0nelrn  44899  cvgdvgrat  45056  binomcxplemdvbinom  45096  eliocre  46258  iccshift  46267  iccsuble  46268  icoiccdif  46273  mullimc  46365  limccog  46369  limciccioolb  46370  mullimcf  46372  limcperiod  46377  lptioo2  46380  lptioo1  46381  neglimc  46394  addlimc  46395  0ellimcdiv  46396  reclimc  46400  xlimmnfvlem1  46579  xlimpnfvlem1  46583  icccncfext  46634  cncfioobdlem  46643  ditgeqiooicc  46707  iblspltprt  46720  iblcncfioo  46725  itgiccshift  46727  itgperiod  46728  itgsbtaddcnst  46729  stoweidlem11  46758  stoweidlem31  46778  stoweidlem36  46783  stoweidlem38  46785  stoweidlem62  46809  dirkercncflem1  46850  dirkercncflem4  46853  fourierdlem26  46880  fourierdlem32  46886  fourierdlem33  46887  fourierdlem37  46891  fourierdlem42  46896  fourierdlem54  46907  fourierdlem63  46916  fourierdlem64  46917  fourierdlem65  46918  fourierdlem74  46927  fourierdlem75  46928  fourierdlem79  46932  fourierdlem81  46934  fourierdlem82  46935  fourierdlem89  46942  fourierdlem90  46943  fourierdlem91  46944  fourierdlem93  46946  fourierdlem101  46954  fourierdlem107  46960  fourierdlem109  46962  fourierdlem111  46964  salunicl  47063  saluncl  47064  hoidmv1lelem1  47338  hoidmv1lelem3  47340  hoidmvlelem1  47342  ovolval3  47394  iinhoiicclem  47420  smfpreimalt  47478  smfpreimaltf  47483  smfpreimale  47501  issmfgt  47503  smfpreimagt  47509  smfpreimage  47529  sigardiv  47608  sigarcol  47611  sharhght  47612  sigaradd  47613  cevathlem1  47614  cevathlem2  47615  cevath  47616  proththd  48399  perfectALTVlem2  48520  gpgnbgrvtx0  48872  gpgnbgrvtx1  48873  imasubc2  49963  imaf1co  49966  idfullsubc  49972  fucofulem1  50121