Theorem simp3d 1150

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simp3bi  1153  f1dom3fv3dif  7219  f1dom3el3dif  7220  oeeui  8535  resixp  8878  domssex2  9072  cantnflem1c  9606  cantnflem1  9608  cantnflem3  9610  cantnflem4  9611  fpwwe2lem6  10557  canthnumlem  10569  canthp1lem2  10574  wununi  10627  wunpw  10628  wunpr  10630  lelttrdi  11306  ixxdisj  13311  ixxun  13312  ixxss1  13314  ixxss2  13315  ixxss12  13316  ixxub  13317  ixxlb  13318  lbioo  13327  elicore  13349  iccsupr  13393  icodisj  13427  xov1plusxeqvd  13449  intfracq  13816  fldiv  13817  seqf1olem2  14002  cjmul  15102  icco1  15500  sumtp  15709  rpnnen2lem10  16188  ruclem2  16197  ruclem3  16198  ruclem9  16203  ruclem12  16206  dvdslegcd  16471  prmdvdsbc  16694  crth  16746  eulerthlem1  16749  eulerthlem2  16750  pcpremul  16812  prmreclem2  16886  prmreclem3  16887  4sqlem13  16926  sectcan  17720  sectco  17721  sectmon  17747  monsect  17748  funcid  17835  funcco  17836  funcsect  17837  invfuc  17942  fuciso  17943  coapm  18036  catciso  18076  postr  18284  ipodrsima  18505  psref2  18534  psasym  18540  mhm0  18760  submcl  18778  submmnd  18779  eqger  19151  eqgcpbl  19155  ghmqusnsglem1  19253  ghmquskerlem1  19256  gaorber  19281  orbsta  19286  cayleyth  19388  pmtrrn2  19433  pmtrfinv  19434  pmtrfmvdn0  19435  dfod2  19537  sylow2blem1  19593  sylow2blem3  19595  dprdcntz  19983  dprddisj  19984  dprdffsupp  19989  dpjdisj  20028  ablfac1a  20044  ablfac1b  20045  lmodvsdir  20883  lmhmlin  21032  lbsind  21077  2idlcpblrng  21271  evlsval3  22072  mpfind  22098  mdetunilem2  22603  mdetunilem5  22606  mdetunilem6  22607  mnfnei  23211  cnprcl  23235  lmcvg  23252  lmff  23291  lmcls  23292  lmcnp  23294  fbasssin  23826  flimfil  23959  tgpconncomp  24103  tlmtrg  24180  ustssel  24196  ustincl  24198  ustdiag  24199  ustinvel  24200  ustexhalf  24201  ustfilxp  24203  tustopn  24260  tususp  24261  imasdsf1olem  24363  xmeter  24423  xmetresbl  24427  tmstopn  24475  metustexhalf  24546  nlmnrg  24669  qdensere  24759  blcvx  24788  tgqioo  24790  icccmplem1  24813  icccmplem2  24814  reconnlem1  24817  cnmpopc  24920  iccpnfcnv  24936  phtpcer  24987  phtpcco2  24991  pcohtpy  25012  pcorev2  25020  pcophtb  25021  om1addcl  25025  pi1blem  25031  pi1cpbl  25036  pi1grplem  25041  pi1inv  25044  pi1xfrf  25045  pi1xfr  25047  pi1xfrcnvlem  25048  pi1cof  25051  pi1coghm  25053  cphreccllem  25170  cphsca  25171  cphsubrg  25172  cphsqrtcl2  25178  phclm  25224  tcphcph  25229  lmmcvg  25253  cmetcaulem  25280  lmcau  25305  bcthlem3  25318  bcthlem4  25319  minveclem4c  25417  minveclem2  25418  minveclem3b  25420  minveclem4  25424  minveclem6  25426  ivthicc  25450  ovollb2lem  25480  ovolshftlem1  25501  ovolscalem1  25505  ovolicc1  25508  ovolicc2lem2  25510  ovolicc2lem3  25511  ovolicc2lem4  25512  ovolicc2lem5  25513  ioombl1lem1  25550  dyadmaxlem  25589  volivth  25599  vitalilem2  25601  vitalilem4  25603  i1fima2  25671  itg2monolem1  25742  itgcnlem  25782  itgrevallem1  25787  itgreval  25789  itgle  25802  ibladd  25813  iblabslem  25820  itgspliticc  25829  itgsplitioo  25830  ditgcl  25850  ditgswap  25851  ditgsplitlem  25852  limcdif  25868  limcresi  25877  limcres  25878  limccnp  25883  limccnp2  25884  limcun  25887  dvlip  25985  dvlip2  25987  dveq0  25992  dvgt0lem1  25994  dvivthlem1  26000  dvcnvrelem1  26009  dvcnvre  26011  dvfsumlem2  26019  ftc1lem1  26027  ftc1lem2  26028  ftc1a  26029  ftc1lem4  26031  ftc2  26036  ftc2ditglem  26037  itgsubstlem  26040  ply1rem  26156  fta1glem2  26159  ig1pdvds  26170  plyrem  26296  fta1lem  26298  vieta1lem2  26302  aaliou3lem3  26335  pserulm  26412  psercnlem2  26414  psercnlem1  26415  psercn  26416  pserdvlem1  26417  pserdvlem2  26418  abelth2  26432  coseq00topi  26491  coseq0negpitopi  26492  cosordlem  26519  tanord1  26526  efif1olem1  26531  dvloglem  26637  efopnlem1  26645  logreclem  26751  relogbval  26761  nnlogbexp  26770  logbrec  26771  chordthmlem4  26824  quart1  26845  quartlem2  26847  quartlem3  26848  quart  26850  acosbnd  26889  atancj  26899  atanlogsublem  26904  atantan  26912  atanbndlem  26914  atans2  26920  dvatan  26924  atantayl  26926  divsqrtsumlem  26968  ftalem5  27065  basellem5  27073  ppisval  27092  chtleppi  27198  chpchtsum  27207  chpub  27208  mersenne  27215  perfectlem2  27218  dchrinv  27249  rplogsumlem2  27473  chpdifbndlem1  27541  pntibndlem2  27579  pntlema  27584  pntlemb  27585  pntlemg  27586  pntlemh  27587  pntlemr  27590  pntlemj  27591  pntlemf  27593  pntlemk  27594  pntlemo  27595  pntlemp  27598  pntleml  27599  abvcxp  27603  ostth2lem2  27622  cutsun12  27807  lesrec  27816  eqcuts3  27821  cofcut2  27939  cofcutr  27941  cofcutrtime  27944  cutmax  27951  cutmin  27952  addsproplem5  27990  addsproplem6  27991  leadds1  28006  addsuniflem  28018  addsasslem1  28020  addsasslem2  28021  negsproplem4  28048  negsproplem6  28050  negcut2  28057  negsunif  28072  mulsproplem12  28144  sltmuls1  28164  sltmuls2  28165  mulsuniflem  28166  precsexlem11  28234  twocut  28440  pw2cut2  28479  axtgcont1  28561  cgr3simp3  28615  legso  28692  hlln  28700  hltr  28703  btwnhl  28707  mirhl  28772  mirbtwnhl  28773  opphllem4  28843  opphl  28847  hlpasch  28849  cgracgr  28911  cgraswap  28913  cgrahl  28920  cgracol  28921  inagswap  28934  inagne3  28937  dfcgrg2  28956  umgrnloopv  29200  umgredgne  29239  usgrnloopvALT  29295  frusgrnn0  29665  cusgrm1rusgr  29676  upgrclwlkcompim  29874  2wlkdlem6  30024  2wlkond  30030  2trlond  30032  numclwwlk2lem1  30471  numclwlk2lem2f1o  30474  tncp  30574  grpolidinv  30597  nvs  30759  nvz  30765  nvtri  30766  sspn  30832  minvecolem2  30971  minvecolem4c  30975  minvecolem4  30976  minvecolem5  30977  minvecolem6  30978  adj1  32029  eliccelico  32876  elicoelioo  32877  pmtrto1cl  33187  cyc3evpm  33238  slmdvsdir  33304  slmd0vs  33312  sdrgdvcl  33390  sdrginvcl  33391  nsgqusf1olem3  33505  prmidl  33530  prmidlc  33538  qsidomlem2  33543  qsnzr  33545  mxidlmax  33555  qsdrnglem2  33586  0ringmon1p  33647  ig1pmindeg  33692  ply1degltdimlem  33813  irngss  33878  ply1annig1p  33895  minplycl  33897  algextdeglem3  33910  algextdeglem4  33911  constrsqrtcl  33970  locfinreflem  34031  cnre2csqlem  34101  sigaclci  34323  unelsiga  34325  insiga  34328  unelldsys  34349  ldsysgenld  34351  sigapildsys  34353  ldgenpisyslem1  34354  measvun  34400  cntmeas  34417  sibfima  34529  signstfveq0  34768  tg5segofs  34864  bnj1018g  35152  bnj1018  35153  pfxwlk  35353  revwlk  35354  spthcycl  35358  acycgrcycl  35376  subfacp1lem3  35411  subfacp1lem4  35412  subfacp1lem5  35413  sconnpht2  35467  sconnpi1  35468  txsconn  35470  resconn  35475  cvmcn  35491  cvmsuni  35498  cvmsdisj  35499  cvmshmeo  35500  cvmlift2lem8  35539  cvmlift2lem13  35544  cvmliftphtlem  35546  cvmliftpht  35547  cvmlift3lem6  35553  msrf  35771  elmsta  35777  mthmpps  35811  mclsppslem  35812  ivthALT  36564  weiunfrlem  36693  weiunfr  36696  relowlssretop  37726  ibladdnc  38045  iblabsnclem  38051  ftc2nc  38070  dvasin  38072  isbndx  38150  isbnd3  38152  prdsbnd  38161  heiborlem3  38181  iccbnd  38208  rngohomadd  38337  rngohommul  38338  idladdcl  38387  idllmulcl  38388  idlrmulcl  38389  maxidlmax  38411  pridlc  38439  eqvreltr  39059  lshpnelb  39477  lshpcmp  39481  oplecon3  39692  opnoncon  39701  hlcvl  39852  dochshpncl  41877  lclkrslem1  42030  lclkrslem2  42031  fzne2d  42466  primrootsunit1  42583  primrootscoprmpow  42585  primrootlekpowne0  42591  aks6d1c1p1  42593  aks6d1c2  42616  sticksstones3  42634  aks5lem1  42672  aks5lem2  42673  aks5lem3a  42675  flt4lem5f  43108  flt4lem7  43110  nna4b4nsq  43111  acongrep  43426  ntrneinex  44522  neicvgmex  44562  gneispace0nelrn  44585  cvgdvgrat  44758  binomcxplemdvbinom  44798  eliocre  45955  iccshift  45964  iccsuble  45965  icoiccdif  45970  mullimc  46062  limccog  46066  limciccioolb  46067  mullimcf  46069  limcperiod  46074  lptioo2  46077  lptioo1  46078  neglimc  46091  addlimc  46092  0ellimcdiv  46093  reclimc  46097  xlimmnfvlem1  46276  xlimpnfvlem1  46280  icccncfext  46331  cncfioobdlem  46340  ditgeqiooicc  46404  iblspltprt  46417  iblcncfioo  46422  itgiccshift  46424  itgperiod  46425  itgsbtaddcnst  46426  stoweidlem11  46455  stoweidlem31  46475  stoweidlem36  46480  stoweidlem38  46482  stoweidlem62  46506  dirkercncflem1  46547  dirkercncflem4  46550  fourierdlem26  46577  fourierdlem32  46583  fourierdlem33  46584  fourierdlem37  46588  fourierdlem42  46593  fourierdlem54  46604  fourierdlem63  46613  fourierdlem64  46614  fourierdlem65  46615  fourierdlem74  46624  fourierdlem75  46625  fourierdlem79  46629  fourierdlem81  46631  fourierdlem82  46632  fourierdlem89  46639  fourierdlem90  46640  fourierdlem91  46641  fourierdlem93  46643  fourierdlem101  46651  fourierdlem107  46657  fourierdlem109  46659  fourierdlem111  46661  salunicl  46760  saluncl  46761  hoidmv1lelem1  47035  hoidmv1lelem3  47037  hoidmvlelem1  47039  ovolval3  47091  iinhoiicclem  47117  smfpreimalt  47175  smfpreimaltf  47180  smfpreimale  47198  issmfgt  47200  smfpreimagt  47206  smfpreimage  47226  sigardiv  47305  sigarcol  47308  sharhght  47309  sigaradd  47310  cevathlem1  47311  cevathlem2  47312  cevath  47313  proththd  48093  perfectALTVlem2  48214  gpgnbgrvtx0  48566  gpgnbgrvtx1  48567  imasubc2  49643  imaf1co  49646  idfullsubc  49652  fucofulem1  49801