Theorem simp3d 1068

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

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  simp3bi  1071  f1dom3fv3dif  6425  f1dom3el3dif  6426  oeeui  7569  erinxp  7708  resixp  7829  domssex2  8005  cantnflem1c  8467  cantnflem1  8469  cantnflem3  8471  cantnflem4  8472  fpwwe2lem7  9337  canthnumlem  9349  canthp1lem2  9354  wununi  9407  wunpw  9408  wunpr  9410  lelttrdi  10078  ixxdisj  12061  ixxun  12062  ixxss1  12064  ixxss2  12065  ixxss12  12066  ixxub  12067  ixxlb  12068  lbioo  12077  elicore  12097  iccsupr  12137  icodisj  12168  xov1plusxeqvd  12189  intfracq  12520  fldiv  12521  seqf1olem2  12703  cjmul  13730  icco1  14119  sumtp  14322  rpnnen2lem10  14791  ruclem2  14800  ruclem3  14801  ruclem9  14806  ruclem12  14809  dvdslegcd  15064  crth  15321  eulerthlem1  15324  eulerthlem2  15325  pcpremul  15386  prmreclem2  15459  prmreclem3  15460  4sqlem13  15499  sectcan  16238  sectco  16239  sectmon  16265  monsect  16266  funcid  16353  funcco  16354  funcsect  16355  invfuc  16457  fuciso  16458  coapm  16544  catciso  16580  postr  16776  ipodrsima  16988  psref2  17027  psasym  17033  mhm0  17166  submcl  17176  submmnd  17177  eqger  17467  eqgcpbl  17471  gaorber  17564  orbsta  17569  cayleyth  17658  pmtrrn2  17703  pmtrfinv  17704  pmtrfmvdn0  17705  dfod2  17804  sylow2blem1  17858  sylow2blem3  17860  dprdcntz  18230  dprddisj  18231  dprdffsupp  18236  dpjdisj  18275  ablfac1a  18291  ablfac1b  18292  lmodvsdir  18710  lmhmlin  18856  lbsind  18901  2idlcpbl  19055  assasca  19142  mpfind  19357  mpt2frlmd  19935  mdetunilem2  20238  mdetunilem5  20241  mdetunilem6  20242  mnfnei  20835  cnprcl  20859  lmcvg  20876  lmff  20915  lmcls  20916  lmcnp  20918  fbasssin  21450  flimfil  21583  tgpconcomp  21726  tlmtrg  21803  ustssel  21819  ustincl  21821  ustdiag  21822  ustinvel  21823  ustexhalf  21824  ustfilxp  21826  tustopn  21885  tususp  21886  imasdsf1olem  21988  xmeter  22048  xmetresbl  22052  tmstopn  22100  metustexhalf  22171  nlmnrg  22293  qdensere  22383  blcvx  22409  tgqioo  22411  icccmplem1  22433  icccmplem2  22434  reconnlem1  22437  cnmpt2pc  22535  iccpnfcnv  22551  phtpcer  22602  phtpcerOLD  22603  phtpcco2  22607  pcohtpy  22628  pcorev2  22636  pcophtb  22637  om1addcl  22641  pi1blem  22647  pi1cpbl  22652  pi1grplem  22657  pi1inv  22660  pi1xfrf  22661  pi1xfr  22663  pi1xfrcnvlem  22664  pi1cof  22667  pi1coghm  22669  cphreccllem  22786  cphsca  22787  cphsubrg  22788  cphsqrtcl2  22794  tchclm  22839  tchcph  22844  lmmcvg  22867  cmetcaulem  22894  lmcau  22919  bcthlem3  22931  bcthlem4  22932  minveclem4c  23004  minveclem2  23005  minveclem3b  23007  minveclem4  23011  minveclem6  23013  ivthicc  23034  ovollb2lem  23063  ovolshftlem1  23084  ovolscalem1  23088  ovolicc1  23091  ovolicc2lem2  23093  ovolicc2lem3  23094  ovolicc2lem4  23095  ovolicc2lem5  23096  ioombl1lem1  23133  dyadmaxlem  23171  volivth  23181  vitalilem2  23184  vitalilem4  23186  i1fima2  23252  itg2monolem1  23323  itgcnlem  23362  itgrevallem1  23367  itgreval  23369  itgle  23382  ibladd  23393  iblabslem  23400  itgspliticc  23409  itgsplitioo  23410  ditgcl  23428  ditgswap  23429  ditgsplitlem  23430  limcdif  23446  limcresi  23455  limcres  23456  limccnp  23461  limccnp2  23462  limcun  23465  dvlip  23560  dvlip2  23562  dveq0  23567  dvgt0lem1  23569  dvivthlem1  23575  dvcnvrelem1  23584  dvcnvre  23586  dvfsumlem2  23594  ftc1lem1  23602  ftc1lem2  23603  ftc1a  23604  ftc1lem4  23606  ftc2  23611  ftc2ditglem  23612  itgsubstlem  23615  ply1rem  23727  fta1glem2  23730  ig1pdvds  23740  plyrem  23864  fta1lem  23866  vieta1lem2  23870  aaliou3lem3  23903  pserulm  23980  psercnlem2  23982  psercnlem1  23983  psercn  23984  pserdvlem1  23985  pserdvlem2  23986  abelth2  24000  coseq00topi  24058  coseq0negpitopi  24059  cosordlem  24081  tanord1  24087  efif1olem1  24092  dvloglem  24194  efopnlem1  24202  logreclem  24300  relogbval  24310  nnlogbexp  24319  logbrec  24320  chordthmlem4  24362  quart1  24383  quartlem2  24385  quartlem3  24386  quart  24388  acosbnd  24427  atancj  24437  atanlogsublem  24442  atantan  24450  atanbndlem  24452  atans2  24458  dvatan  24462  atantayl  24464  divsqrtsumlem  24506  ftalem5  24603  basellem5  24611  ppisval  24630  chtleppi  24735  chpchtsum  24744  chpub  24745  mersenne  24752  perfectlem2  24755  dchrinv  24786  rplogsumlem2  24974  chpdifbndlem1  25042  pntibndlem2  25080  pntlema  25085  pntlemb  25086  pntlemg  25087  pntlemh  25088  pntlemr  25091  pntlemj  25092  pntlemf  25094  pntlemk  25095  pntlemo  25096  pntlemp  25099  pntleml  25100  abvcxp  25104  ostth2lem2  25123  axtgcont1  25167  cgr3simp3  25217  legso  25294  hlln  25302  hltr  25305  btwnhl  25309  mirhl  25374  mirbtwnhl  25375  opphllem4  25442  opphl  25446  hlpasch  25448  cgracgr  25510  cgraswap  25512  cgrahl  25518  cgracol  25519  inagswap  25530  umgrnloopv  25772  umgredgne  25816  wlkonwlk  26065  wwlksswrd  26216  wwlkeq  26250  clwwisshclwwn  26336  erclwwlksym  26342  erclwwlktr  26343  el2wlksoton  26405  el2spthsoton  26406  cusgraiffrusgra  26467  eupapf  26499  frrusgraord  26598  tncp  26721  grpolidinv  26739  nvs  26902  nvz  26908  nvtri  26909  sspn  26975  minvecolem2  27115  minvecolem4c  27119  minvecolem4  27120  minvecolem5  27121  minvecolem6  27122  adj1  28176  eliccelico  28929  elicoelioo  28930  slmdvsdir  29100  slmd0vs  29108  pmtrto1cl  29180  locfinreflem  29235  cnre2csqlem  29284  sigaclci  29522  unelsiga  29524  insiga  29527  unelldsys  29548  ldsysgenld  29550  sigapildsys  29552  ldgenpisyslem1  29553  measvun  29599  cntmeas  29616  sibfima  29727  signstfveq0  29980  tg5segofs  30004  bnj1018  30286  subfacp1lem3  30418  subfacp1lem4  30419  subfacp1lem5  30420  sconpht2  30474  sconpi1  30475  txscon  30477  rescon  30482  cvmcn  30498  cvmsuni  30505  cvmsdisj  30506  cvmshmeo  30507  cvmlift2lem8  30546  cvmlift2lem13  30551  cvmliftphtlem  30553  cvmliftpht  30554  cvmlift3lem6  30560  msrf  30693  elmsta  30699  mthmpps  30733  mclsppslem  30734  ivthALT  31500  relowlssretop  32387  ibladdnc  32637  iblabsnclem  32643  ftc2nc  32664  dvasin  32666  isbndx  32751  isbnd3  32753  prdsbnd  32762  heiborlem3  32782  iccbnd  32809  rngohomadd  32938  rngohommul  32939  idladdcl  32988  idllmulcl  32989  idlrmulcl  32990  maxidlmax  33012  pridlc  33040  lshpnelb  33289  lshpcmp  33293  oplecon3  33504  opnoncon  33513  hlcvl  33664  dochshpncl  35691  lclkrslem1  35844  lclkrslem2  35845  acongrep  36565  ntrneinex  37395  neicvgmex  37435  gneispace0nelrn  37458  cvgdvgrat  37534  binomcxplemdvbinom  37574  fvixp2  38384  eliocre  38581  iccshift  38591  iccsuble  38592  icoiccdif  38597  mullimc  38683  limccog  38687  limciccioolb  38688  mullimcf  38690  limcperiod  38695  lptioo2  38698  lptioo1  38699  neglimc  38714  addlimc  38715  0ellimcdiv  38716  reclimc  38720  icccncfext  38773  cncfioobdlem  38782  ditgeqiooicc  38852  iblspltprt  38865  iblcncfioo  38870  itgiccshift  38872  itgperiod  38873  itgsbtaddcnst  38874  stoweidlem11  38904  stoweidlem31  38924  stoweidlem36  38929  stoweidlem38  38931  stoweidlem62  38955  dirkercncflem1  38996  dirkercncflem4  38999  fourierdlem26  39026  fourierdlem32  39032  fourierdlem33  39033  fourierdlem37  39037  fourierdlem42  39042  fourierdlem54  39053  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem74  39073  fourierdlem75  39074  fourierdlem79  39078  fourierdlem81  39080  fourierdlem82  39081  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem93  39092  fourierdlem101  39100  fourierdlem107  39106  fourierdlem109  39108  fourierdlem111  39110  salunicl  39212  saluncl  39213  hoidmv1lelem1  39481  hoidmv1lelem3  39483  hoidmvlelem1  39485  ovolval3  39537  iinhoiicclem  39564  smfpreimalt  39617  smfpreimaltf  39623  smfpreimale  39641  issmfgt  39643  smfpreimagt  39648  smfpreimage  39668  sigardiv  39699  sigarcol  39702  sharhght  39703  sigaradd  39704  cevathlem1  39705  cevathlem2  39706  cevath  39707  proththd  40069  perfectALTVlem2  40165  usgrnloopvALT  40428  frusgrnn0  40771  cusgrm1rusgr  40782  upgrclwlkcompim  40988  21wlkdlem6  41138  21wlkond  41144  2trlond  41146  av-numclwwlk2lem1  41532