Theorem simp3d 1141

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 206  df-an 396  df-3an 1086

This theorem is referenced by:  simp3bi  1144  f1dom3fv3dif  7259  f1dom3el3dif  7260  oeeui  8597  resixp  8923  domssex2  9133  cantnflem1c  9678  cantnflem1  9680  cantnflem3  9682  cantnflem4  9683  fpwwe2lem6  10627  canthnumlem  10639  canthp1lem2  10644  wununi  10697  wunpw  10698  wunpr  10700  lelttrdi  11373  ixxdisj  13336  ixxun  13337  ixxss1  13339  ixxss2  13340  ixxss12  13341  ixxub  13342  ixxlb  13343  lbioo  13352  elicore  13373  iccsupr  13416  icodisj  13450  xov1plusxeqvd  13472  intfracq  13821  fldiv  13822  seqf1olem2  14005  cjmul  15086  icco1  15481  sumtp  15692  rpnnen2lem10  16163  ruclem2  16172  ruclem3  16173  ruclem9  16178  ruclem12  16181  dvdslegcd  16442  prmdvdsbc  16661  crth  16710  eulerthlem1  16713  eulerthlem2  16714  pcpremul  16775  prmreclem2  16849  prmreclem3  16850  4sqlem13  16889  sectcan  17701  sectco  17702  sectmon  17728  monsect  17729  funcid  17819  funcco  17820  funcsect  17821  invfuc  17929  fuciso  17930  coapm  18023  catciso  18063  postr  18275  ipodrsima  18496  psref2  18525  psasym  18531  mhm0  18714  submcl  18727  submmnd  18728  eqger  19095  eqgcpbl  19099  gaorber  19214  orbsta  19219  cayleyth  19325  pmtrrn2  19370  pmtrfinv  19371  pmtrfmvdn0  19372  dfod2  19474  sylow2blem1  19530  sylow2blem3  19532  dprdcntz  19920  dprddisj  19921  dprdffsupp  19926  dpjdisj  19965  ablfac1a  19981  ablfac1b  19982  lmodvsdir  20722  lmhmlin  20873  lbsind  20918  2idlcpblrng  21118  mpfind  21980  mdetunilem2  22437  mdetunilem5  22440  mdetunilem6  22441  mnfnei  23047  cnprcl  23071  lmcvg  23088  lmff  23127  lmcls  23128  lmcnp  23130  fbasssin  23662  flimfil  23795  tgpconncomp  23939  tlmtrg  24016  ustssel  24032  ustincl  24034  ustdiag  24035  ustinvel  24036  ustexhalf  24037  ustfilxp  24039  tustopn  24098  tususp  24099  imasdsf1olem  24201  xmeter  24261  xmetresbl  24265  tmstopn  24316  metustexhalf  24387  nlmnrg  24518  qdensere  24608  blcvx  24636  tgqioo  24638  icccmplem1  24660  icccmplem2  24661  reconnlem1  24664  cnmpopc  24771  iccpnfcnv  24791  phtpcer  24843  phtpcco2  24848  pcohtpy  24869  pcorev2  24877  pcophtb  24878  om1addcl  24882  pi1blem  24888  pi1cpbl  24893  pi1grplem  24898  pi1inv  24901  pi1xfrf  24902  pi1xfr  24904  pi1xfrcnvlem  24905  pi1cof  24908  pi1coghm  24910  cphreccllem  25028  cphsca  25029  cphsubrg  25030  cphsqrtcl2  25036  phclm  25082  tcphcph  25087  lmmcvg  25111  cmetcaulem  25138  lmcau  25163  bcthlem3  25176  bcthlem4  25177  minveclem4c  25275  minveclem2  25276  minveclem3b  25278  minveclem4  25282  minveclem6  25284  ivthicc  25309  ovollb2lem  25339  ovolshftlem1  25360  ovolscalem1  25364  ovolicc1  25367  ovolicc2lem2  25369  ovolicc2lem3  25370  ovolicc2lem4  25371  ovolicc2lem5  25372  ioombl1lem1  25409  dyadmaxlem  25448  volivth  25458  vitalilem2  25460  vitalilem4  25462  i1fima2  25530  itg2monolem1  25602  itgcnlem  25641  itgrevallem1  25646  itgreval  25648  itgle  25661  ibladd  25672  iblabslem  25679  itgspliticc  25688  itgsplitioo  25689  ditgcl  25709  ditgswap  25710  ditgsplitlem  25711  limcdif  25727  limcresi  25736  limcres  25737  limccnp  25742  limccnp2  25743  limcun  25746  dvlip  25848  dvlip2  25850  dveq0  25855  dvgt0lem1  25857  dvivthlem1  25863  dvcnvrelem1  25872  dvcnvre  25874  dvfsumlem2  25883  dvfsumlem2OLD  25884  ftc1lem1  25892  ftc1lem2  25893  ftc1a  25894  ftc1lem4  25896  ftc2  25901  ftc2ditglem  25902  itgsubstlem  25905  ply1rem  26021  fta1glem2  26024  ig1pdvds  26034  plyrem  26159  fta1lem  26161  vieta1lem2  26165  aaliou3lem3  26198  pserulm  26275  psercnlem2  26278  psercnlem1  26279  psercn  26280  pserdvlem1  26281  pserdvlem2  26282  abelth2  26296  coseq00topi  26354  coseq0negpitopi  26355  cosordlem  26381  tanord1  26388  efif1olem1  26393  dvloglem  26498  efopnlem1  26506  logreclem  26610  relogbval  26620  nnlogbexp  26629  logbrec  26630  chordthmlem4  26683  quart1  26704  quartlem2  26706  quartlem3  26707  quart  26709  acosbnd  26748  atancj  26758  atanlogsublem  26763  atantan  26771  atanbndlem  26773  atans2  26779  dvatan  26783  atantayl  26785  divsqrtsumlem  26828  ftalem5  26925  basellem5  26933  ppisval  26952  chtleppi  27059  chpchtsum  27068  chpub  27069  mersenne  27076  perfectlem2  27079  dchrinv  27110  rplogsumlem2  27334  chpdifbndlem1  27402  pntibndlem2  27440  pntlema  27445  pntlemb  27446  pntlemg  27447  pntlemh  27448  pntlemr  27451  pntlemj  27452  pntlemf  27454  pntlemk  27455  pntlemo  27456  pntlemp  27459  pntleml  27460  abvcxp  27464  ostth2lem2  27483  scutun12  27659  slerec  27668  cofcut2  27758  cofcutr  27760  cofcutrtime  27763  addsproplem5  27806  addsproplem6  27807  sleadd1  27822  addsuniflem  27834  addsasslem1  27836  addsasslem2  27837  negsproplem4  27859  negsproplem6  27861  negscut2  27868  negsunif  27883  mulsproplem12  27943  ssltmul1  27963  ssltmul2  27964  mulsuniflem  27965  precsexlem11  28031  axtgcont1  28188  cgr3simp3  28242  legso  28319  hlln  28327  hltr  28330  btwnhl  28334  mirhl  28399  mirbtwnhl  28400  opphllem4  28470  opphl  28474  hlpasch  28476  cgracgr  28538  cgraswap  28540  cgrahl  28547  cgracol  28548  inagswap  28561  inagne3  28564  dfcgrg2  28583  umgrnloopv  28835  umgredgne  28874  usgrnloopvALT  28927  frusgrnn0  29297  cusgrm1rusgr  29308  upgrclwlkcompim  29507  2wlkdlem6  29654  2wlkond  29660  2trlond  29662  numclwwlk2lem1  30098  numclwlk2lem2f1o  30101  tncp  30200  grpolidinv  30223  nvs  30385  nvz  30391  nvtri  30392  sspn  30458  minvecolem2  30597  minvecolem4c  30601  minvecolem4  30602  minvecolem5  30603  minvecolem6  30604  adj1  31655  eliccelico  32457  elicoelioo  32458  pmtrto1cl  32726  cyc3evpm  32777  slmdvsdir  32829  slmd0vs  32837  sdrgdvcl  32863  sdrginvcl  32864  nsgqusf1olem3  32995  ghmquskerlem1  32997  prmidl  33027  prmidlc  33036  qsidomlem2  33041  qsnzr  33043  mxidlmax  33050  qsdrnglem2  33079  0ringmon1p  33104  ig1pmindeg  33138  ply1degltdimlem  33186  irngss  33231  ply1annig1p  33245  minplycl  33247  algextdeglem3  33255  algextdeglem4  33256  locfinreflem  33309  cnre2csqlem  33379  sigaclci  33619  unelsiga  33621  insiga  33624  unelldsys  33645  ldsysgenld  33647  sigapildsys  33649  ldgenpisyslem1  33650  measvun  33696  cntmeas  33713  sibfima  33826  signstfveq0  34077  tg5segofs  34174  bnj1018g  34463  bnj1018  34464  pfxwlk  34603  revwlk  34604  spthcycl  34609  acycgrcycl  34627  subfacp1lem3  34662  subfacp1lem4  34663  subfacp1lem5  34664  sconnpht2  34718  sconnpi1  34719  txsconn  34721  resconn  34726  cvmcn  34742  cvmsuni  34749  cvmsdisj  34750  cvmshmeo  34751  cvmlift2lem8  34790  cvmlift2lem13  34795  cvmliftphtlem  34797  cvmliftpht  34798  cvmlift3lem6  34804  msrf  35022  elmsta  35028  mthmpps  35062  mclsppslem  35063  ivthALT  35710  relowlssretop  36734  ibladdnc  37035  iblabsnclem  37041  ftc2nc  37060  dvasin  37062  isbndx  37140  isbnd3  37142  prdsbnd  37151  heiborlem3  37171  iccbnd  37198  rngohomadd  37327  rngohommul  37328  idladdcl  37377  idllmulcl  37378  idlrmulcl  37379  maxidlmax  37401  pridlc  37429  eqvreltr  37967  lshpnelb  38344  lshpcmp  38348  oplecon3  38559  opnoncon  38568  hlcvl  38719  dochshpncl  40745  lclkrslem1  40898  lclkrslem2  40899  fzne2d  41339  sticksstones3  41457  metakunt8  41485  metakunt20  41497  metakunt21  41498  metakunt22  41499  metakunt24  41501  metakunt25  41502  evlsval3  41620  flt4lem5f  41888  flt4lem7  41890  nna4b4nsq  41891  acongrep  42208  ntrneinex  43317  neicvgmex  43357  gneispace0nelrn  43380  cvgdvgrat  43561  binomcxplemdvbinom  43601  eliocre  44707  iccshift  44716  iccsuble  44717  icoiccdif  44722  mullimc  44817  limccog  44821  limciccioolb  44822  mullimcf  44824  limcperiod  44829  lptioo2  44832  lptioo1  44833  neglimc  44848  addlimc  44849  0ellimcdiv  44850  reclimc  44854  xlimmnfvlem1  45033  xlimpnfvlem1  45037  icccncfext  45088  cncfioobdlem  45097  ditgeqiooicc  45161  iblspltprt  45174  iblcncfioo  45179  itgiccshift  45181  itgperiod  45182  itgsbtaddcnst  45183  stoweidlem11  45212  stoweidlem31  45232  stoweidlem36  45237  stoweidlem38  45239  stoweidlem62  45263  dirkercncflem1  45304  dirkercncflem4  45307  fourierdlem26  45334  fourierdlem32  45340  fourierdlem33  45341  fourierdlem37  45345  fourierdlem42  45350  fourierdlem54  45361  fourierdlem63  45370  fourierdlem64  45371  fourierdlem65  45372  fourierdlem74  45381  fourierdlem75  45382  fourierdlem79  45386  fourierdlem81  45388  fourierdlem82  45389  fourierdlem89  45396  fourierdlem90  45397  fourierdlem91  45398  fourierdlem93  45400  fourierdlem101  45408  fourierdlem107  45414  fourierdlem109  45416  fourierdlem111  45418  salunicl  45517  saluncl  45518  hoidmv1lelem1  45792  hoidmv1lelem3  45794  hoidmvlelem1  45796  ovolval3  45848  iinhoiicclem  45874  smfpreimalt  45932  smfpreimaltf  45937  smfpreimale  45955  issmfgt  45957  smfpreimagt  45963  smfpreimage  45983  sigardiv  46062  sigarcol  46065  sharhght  46066  sigaradd  46067  cevathlem1  46068  cevathlem2  46069  cevath  46070  proththd  46767  perfectALTVlem2  46875