Theorem simp3d 1144

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 1138	. 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simp3bi  1147  f1dom3fv3dif  7251  f1dom3el3dif  7252  oeeui  8585  resixp  8910  domssex2  9120  cantnflem1c  9664  cantnflem1  9666  cantnflem3  9668  cantnflem4  9669  fpwwe2lem6  10613  canthnumlem  10625  canthp1lem2  10630  wununi  10683  wunpw  10684  wunpr  10686  lelttrdi  11358  ixxdisj  13321  ixxun  13322  ixxss1  13324  ixxss2  13325  ixxss12  13326  ixxub  13327  ixxlb  13328  lbioo  13337  elicore  13358  iccsupr  13401  icodisj  13435  xov1plusxeqvd  13457  intfracq  13806  fldiv  13807  seqf1olem2  13990  cjmul  15071  icco1  15466  sumtp  15677  rpnnen2lem10  16148  ruclem2  16157  ruclem3  16158  ruclem9  16163  ruclem12  16166  dvdslegcd  16427  crth  16693  eulerthlem1  16696  eulerthlem2  16697  pcpremul  16758  prmreclem2  16832  prmreclem3  16833  4sqlem13  16872  sectcan  17684  sectco  17685  sectmon  17711  monsect  17712  funcid  17802  funcco  17803  funcsect  17804  invfuc  17909  fuciso  17910  coapm  18003  catciso  18043  postr  18255  ipodrsima  18476  psref2  18505  psasym  18511  mhm0  18656  submcl  18669  submmnd  18670  eqger  19030  eqgcpbl  19034  gaorber  19138  orbsta  19143  cayleyth  19247  pmtrrn2  19292  pmtrfinv  19293  pmtrfmvdn0  19294  dfod2  19396  sylow2blem1  19452  sylow2blem3  19454  dprdcntz  19837  dprddisj  19838  dprdffsupp  19843  dpjdisj  19882  ablfac1a  19898  ablfac1b  19899  lmodvsdir  20445  lmhmlin  20595  lbsind  20640  2idlcpbl  20807  mpfind  21599  mdetunilem2  22044  mdetunilem5  22047  mdetunilem6  22048  mnfnei  22654  cnprcl  22678  lmcvg  22695  lmff  22734  lmcls  22735  lmcnp  22737  fbasssin  23269  flimfil  23402  tgpconncomp  23546  tlmtrg  23623  ustssel  23639  ustincl  23641  ustdiag  23642  ustinvel  23643  ustexhalf  23644  ustfilxp  23646  tustopn  23705  tususp  23706  imasdsf1olem  23808  xmeter  23868  xmetresbl  23872  tmstopn  23923  metustexhalf  23994  nlmnrg  24125  qdensere  24215  blcvx  24243  tgqioo  24245  icccmplem1  24267  icccmplem2  24268  reconnlem1  24271  cnmpopc  24373  iccpnfcnv  24389  phtpcer  24440  phtpcco2  24444  pcohtpy  24465  pcorev2  24473  pcophtb  24474  om1addcl  24478  pi1blem  24484  pi1cpbl  24489  pi1grplem  24494  pi1inv  24497  pi1xfrf  24498  pi1xfr  24500  pi1xfrcnvlem  24501  pi1cof  24504  pi1coghm  24506  cphreccllem  24624  cphsca  24625  cphsubrg  24626  cphsqrtcl2  24632  phclm  24678  tcphcph  24683  lmmcvg  24707  cmetcaulem  24734  lmcau  24759  bcthlem3  24772  bcthlem4  24773  minveclem4c  24871  minveclem2  24872  minveclem3b  24874  minveclem4  24878  minveclem6  24880  ivthicc  24904  ovollb2lem  24934  ovolshftlem1  24955  ovolscalem1  24959  ovolicc1  24962  ovolicc2lem2  24964  ovolicc2lem3  24965  ovolicc2lem4  24966  ovolicc2lem5  24967  ioombl1lem1  25004  dyadmaxlem  25043  volivth  25053  vitalilem2  25055  vitalilem4  25057  i1fima2  25125  itg2monolem1  25197  itgcnlem  25236  itgrevallem1  25241  itgreval  25243  itgle  25256  ibladd  25267  iblabslem  25274  itgspliticc  25283  itgsplitioo  25284  ditgcl  25304  ditgswap  25305  ditgsplitlem  25306  limcdif  25322  limcresi  25331  limcres  25332  limccnp  25337  limccnp2  25338  limcun  25341  dvlip  25439  dvlip2  25441  dveq0  25446  dvgt0lem1  25448  dvivthlem1  25454  dvcnvrelem1  25463  dvcnvre  25465  dvfsumlem2  25473  ftc1lem1  25481  ftc1lem2  25482  ftc1a  25483  ftc1lem4  25485  ftc2  25490  ftc2ditglem  25491  itgsubstlem  25494  ply1rem  25610  fta1glem2  25613  ig1pdvds  25623  plyrem  25747  fta1lem  25749  vieta1lem2  25753  aaliou3lem3  25786  pserulm  25863  psercnlem2  25865  psercnlem1  25866  psercn  25867  pserdvlem1  25868  pserdvlem2  25869  abelth2  25883  coseq00topi  25941  coseq0negpitopi  25942  cosordlem  25968  tanord1  25975  efif1olem1  25980  dvloglem  26085  efopnlem1  26093  logreclem  26194  relogbval  26204  nnlogbexp  26213  logbrec  26214  chordthmlem4  26267  quart1  26288  quartlem2  26290  quartlem3  26291  quart  26293  acosbnd  26332  atancj  26342  atanlogsublem  26347  atantan  26355  atanbndlem  26357  atans2  26363  dvatan  26367  atantayl  26369  divsqrtsumlem  26411  ftalem5  26508  basellem5  26516  ppisval  26535  chtleppi  26640  chpchtsum  26649  chpub  26650  mersenne  26657  perfectlem2  26660  dchrinv  26691  rplogsumlem2  26915  chpdifbndlem1  26983  pntibndlem2  27021  pntlema  27026  pntlemb  27027  pntlemg  27028  pntlemh  27029  pntlemr  27032  pntlemj  27033  pntlemf  27035  pntlemk  27036  pntlemo  27037  pntlemp  27040  pntleml  27041  abvcxp  27045  ostth2lem2  27064  scutun12  27237  slerec  27246  cofcut2  27329  cofcutr  27331  cofcutrtime  27334  addsproplem5  27373  addsproplem6  27374  sleadd1  27388  addsuniflem  27400  addsasslem1  27402  addsasslem2  27403  negsproplem4  27421  negsproplem6  27423  negscut2  27430  negsunif  27443  mulsproplem12  27496  ssltmul1  27514  ssltmul2  27515  mulsuniflem  27516  axtgcont1  27584  cgr3simp3  27638  legso  27715  hlln  27723  hltr  27726  btwnhl  27730  mirhl  27795  mirbtwnhl  27796  opphllem4  27866  opphl  27870  hlpasch  27872  cgracgr  27934  cgraswap  27936  cgrahl  27943  cgracol  27944  inagswap  27957  inagne3  27960  dfcgrg2  27979  umgrnloopv  28231  umgredgne  28270  usgrnloopvALT  28323  frusgrnn0  28693  cusgrm1rusgr  28704  upgrclwlkcompim  28903  2wlkdlem6  29050  2wlkond  29056  2trlond  29058  numclwwlk2lem1  29494  numclwlk2lem2f1o  29497  tncp  29594  grpolidinv  29617  nvs  29779  nvz  29785  nvtri  29786  sspn  29852  minvecolem2  29991  minvecolem4c  29995  minvecolem4  29996  minvecolem5  29997  minvecolem6  29998  adj1  31049  eliccelico  31859  elicoelioo  31860  prmdvdsbc  31893  pmtrto1cl  32129  cyc3evpm  32180  slmdvsdir  32232  slmd0vs  32240  sdrgdvcl  32259  sdrginvcl  32260  nsgqusf1olem3  32382  ghmquskerlem1  32384  prmidl  32409  prmidlc  32418  qsidomlem2  32423  qsnzr  32425  mxidlmax  32432  qsdrnglem2  32456  0ringmon1p  32481  ply1degltdimlem  32545  irngss  32589  ply1annig1p  32601  locfinreflem  32651  cnre2csqlem  32721  sigaclci  32961  unelsiga  32963  insiga  32966  unelldsys  32987  ldsysgenld  32989  sigapildsys  32991  ldgenpisyslem1  32992  measvun  33038  cntmeas  33055  sibfima  33168  signstfveq0  33419  tg5segofs  33516  bnj1018g  33805  bnj1018  33806  pfxwlk  33945  revwlk  33946  spthcycl  33951  acycgrcycl  33969  subfacp1lem3  34004  subfacp1lem4  34005  subfacp1lem5  34006  sconnpht2  34060  sconnpi1  34061  txsconn  34063  resconn  34068  cvmcn  34084  cvmsuni  34091  cvmsdisj  34092  cvmshmeo  34093  cvmlift2lem8  34132  cvmlift2lem13  34137  cvmliftphtlem  34139  cvmliftpht  34140  cvmlift3lem6  34146  msrf  34364  elmsta  34370  mthmpps  34404  mclsppslem  34405  ivthALT  35024  relowlssretop  36048  ibladdnc  36349  iblabsnclem  36355  ftc2nc  36374  dvasin  36376  isbndx  36455  isbnd3  36457  prdsbnd  36466  heiborlem3  36486  iccbnd  36513  rngohomadd  36642  rngohommul  36643  idladdcl  36692  idllmulcl  36693  idlrmulcl  36694  maxidlmax  36716  pridlc  36744  eqvreltr  37282  lshpnelb  37659  lshpcmp  37663  oplecon3  37874  opnoncon  37883  hlcvl  38034  dochshpncl  40060  lclkrslem1  40213  lclkrslem2  40214  fzne2d  40651  sticksstones3  40769  metakunt8  40797  metakunt20  40809  metakunt21  40810  metakunt22  40811  metakunt24  40813  metakunt25  40814  evlsval3  40930  flt4lem5f  41181  flt4lem7  41183  nna4b4nsq  41184  acongrep  41490  ntrneinex  42599  neicvgmex  42639  gneispace0nelrn  42662  cvgdvgrat  42843  binomcxplemdvbinom  42883  eliocre  43995  iccshift  44004  iccsuble  44005  icoiccdif  44010  mullimc  44105  limccog  44109  limciccioolb  44110  mullimcf  44112  limcperiod  44117  lptioo2  44120  lptioo1  44121  neglimc  44136  addlimc  44137  0ellimcdiv  44138  reclimc  44142  xlimmnfvlem1  44321  xlimpnfvlem1  44325  icccncfext  44376  cncfioobdlem  44385  ditgeqiooicc  44449  iblspltprt  44462  iblcncfioo  44467  itgiccshift  44469  itgperiod  44470  itgsbtaddcnst  44471  stoweidlem11  44500  stoweidlem31  44520  stoweidlem36  44525  stoweidlem38  44527  stoweidlem62  44551  dirkercncflem1  44592  dirkercncflem4  44595  fourierdlem26  44622  fourierdlem32  44628  fourierdlem33  44629  fourierdlem37  44633  fourierdlem42  44638  fourierdlem54  44649  fourierdlem63  44658  fourierdlem64  44659  fourierdlem65  44660  fourierdlem74  44669  fourierdlem75  44670  fourierdlem79  44674  fourierdlem81  44676  fourierdlem82  44677  fourierdlem89  44684  fourierdlem90  44685  fourierdlem91  44686  fourierdlem93  44688  fourierdlem101  44696  fourierdlem107  44702  fourierdlem109  44704  fourierdlem111  44706  salunicl  44805  saluncl  44806  hoidmv1lelem1  45080  hoidmv1lelem3  45082  hoidmvlelem1  45084  ovolval3  45136  iinhoiicclem  45162  smfpreimalt  45220  smfpreimaltf  45225  smfpreimale  45243  issmfgt  45245  smfpreimagt  45251  smfpreimage  45271  sigardiv  45350  sigarcol  45353  sharhght  45354  sigaradd  45355  cevathlem1  45356  cevathlem2  45357  cevath  45358  proththd  46054  perfectALTVlem2  46162