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  7272  f1dom3el3dif  7273  oeeui  8614  resixp  8964  domssex2  9159  cantnflem1c  9691  cantnflem1  9693  cantnflem3  9695  cantnflem4  9696  fpwwe2lem6  10724  canthnumlem  10736  canthp1lem2  10741  wununi  10794  wunpw  10795  wunpr  10797  lelttrdi  11475  ixxdisj  13494  ixxun  13495  ixxss1  13497  ixxss2  13498  ixxss12  13499  ixxub  13500  ixxlb  13501  lbioo  13510  elicore  13532  iccsupr  13576  icodisj  13610  xov1plusxeqvd  13632  intfracq  14002  fldiv  14003  seqf1olem2  14188  cjmul  15314  icco1  15712  sumtp  15920  rpnnen2lem10  16396  ruclem2  16405  ruclem3  16406  ruclem9  16411  ruclem12  16414  dvdslegcd  16679  prmdvdsbc  16907  crth  16960  eulerthlem1  16963  eulerthlem2  16964  pcpremul  17026  prmreclem2  17100  prmreclem3  17101  4sqlem13  17140  sectcan  17935  sectco  17936  sectmon  17962  monsect  17963  funcid  18050  funcco  18051  funcsect  18052  invfuc  18157  fuciso  18158  coapm  18251  catciso  18291  postr  18499  ipodrsima  18720  psref2  18749  psasym  18755  mhm0  18994  submcl  19012  submmnd  19014  eqger  19395  eqgcpbl  19399  ghmqusnsglem1  19499  ghmquskerlem1  19502  gaorber  19527  orbsta  19532  cayleyth  19634  pmtrrn2  19679  pmtrfinv  19680  pmtrfmvdn0  19681  dfod2  19783  sylow2blem1  19839  sylow2blem3  19841  dprdcntz  20229  dprddisj  20230  dprdffsupp  20235  dpjdisj  20274  ablfac1a  20290  ablfac1b  20291  lmodvsdir  21166  lmhmlin  21315  lbsind  21360  2idlcpblrng  21570  prmidl  21626  prmidlc  21634  prmidlprop  21637  qsidomlem2  21642  qsnzr  21644  evlsval3  22403  mpfind  22429  mdetunilem2  22933  mdetunilem5  22936  mdetunilem6  22937  mnfnei  23544  cnprcl  23568  lmcvg  23585  lmff  23624  lmcls  23625  lmcnp  23627  fbasssin  24160  flimfil  24293  tgpconncomp  24437  tlmtrg  24514  ustssel  24530  ustincl  24532  ustdiag  24533  ustinvel  24534  ustexhalf  24535  ustfilxp  24537  tustopn  24594  tususp  24595  imasdsf1olem  24697  xmeter  24757  xmetresbl  24761  tmstopn  24809  metustexhalf  24880  nlmnrg  25003  qdensere  25093  blcvx  25122  tgqioo  25124  icccmplem1  25147  icccmplem2  25148  reconnlem1  25151  cnmpopc  25254  iccpnfcnv  25270  phtpcer  25321  phtpcco2  25325  pcohtpy  25346  pcorev2  25354  pcophtb  25355  om1addcl  25359  pi1blem  25365  pi1cpbl  25370  pi1grplem  25375  pi1inv  25378  pi1xfrf  25379  pi1xfr  25381  pi1xfrcnvlem  25382  pi1cof  25385  pi1coghm  25387  cphreccllem  25504  cphsca  25505  cphsubrg  25506  cphsqrtcl2  25512  phclm  25558  tcphcph  25563  lmmcvg  25587  cmetcaulem  25614  lmcau  25639  bcthlem3  25652  bcthlem4  25653  minveclem4c  25751  minveclem2  25752  minveclem3b  25754  minveclem4  25758  minveclem6  25760  ivthicc  25784  ovollb2lem  25814  ovolshftlem1  25835  ovolscalem1  25839  ovolicc1  25842  ovolicc2lem2  25844  ovolicc2lem3  25845  ovolicc2lem4  25846  ovolicc2lem5  25847  ioombl1lem1  25884  dyadmaxlem  25923  volivth  25933  vitalilem2  25935  vitalilem4  25937  i1fima2  26005  itg2monolem1  26076  itgcnlem  26115  itgrevallem1  26120  itgreval  26122  itgle  26135  ibladd  26146  iblabslem  26153  itgspliticc  26162  itgsplitioo  26163  ditgcl  26183  ditgswap  26184  ditgsplitlem  26185  limcdif  26201  limcresi  26210  limcres  26211  limccnp  26216  limccnp2  26217  limcun  26220  dvlip  26318  dvlip2  26320  dveq0  26325  dvgt0lem1  26327  dvivthlem1  26333  dvcnvrelem1  26342  dvcnvre  26344  dvfsumlem2  26352  ftc1lem1  26360  ftc1lem2  26361  ftc1a  26362  ftc1lem4  26364  ftc2  26369  ftc2ditglem  26370  itgsubstlem  26373  ply1rem  26489  fta1glem2  26492  ig1pdvds  26503  plyrem  26631  fta1lem  26633  vieta1lem2  26639  aaliou3lem3  26676  pserulm  26754  psercnlem2  26756  psercnlem1  26757  psercn  26758  pserdvlem1  26759  pserdvlem2  26760  abelth2  26774  coseq00topi  26836  coseq0negpitopi  26837  cosordlem  26863  tanord1  26870  efif1olem1  26875  dvloglem  26981  efopnlem1  26989  logreclem  27095  relogbval  27105  nnlogbexp  27114  logbrec  27115  chordthmlem4  27168  quart1  27189  quartlem2  27191  quartlem3  27192  quart  27194  acosbnd  27233  atancj  27243  atanlogsublem  27248  atantan  27256  atanbndlem  27258  atans2  27264  dvatan  27268  atantayl  27270  divsqrtsumlem  27312  ftalem5  27409  basellem5  27417  ppisval  27436  chtleppi  27542  chpchtsum  27551  chpub  27552  mersenne  27559  perfectlem2  27562  dchrinv  27593  rplogsumlem2  27817  chpdifbndlem1  27885  pntibndlem2  27923  pntlema  27928  pntlemb  27929  pntlemg  27930  pntlemh  27931  pntlemr  27934  pntlemj  27935  pntlemf  27937  pntlemk  27938  pntlemo  27939  pntlemp  27942  pntleml  27943  abvcxp  27947  ostth2lem2  27966  flt4lem5f  27992  flt4lem7  27994  nna4b4nsq  27995  cutsun12  28181  lesrec  28190  eqcuts3  28195  cofcut2  28313  cofcutr  28315  cofcutrtime  28318  cutmax  28325  cutmin  28326  addsproplem5  28364  addsproplem6  28365  leadds1  28380  addsuniflem  28392  addsasslem1  28394  addsasslem2  28395  negsproplem4  28422  negsproplem6  28424  negcut2  28431  negsunif  28446  mulsproplem12  28518  sltmuls1  28538  sltmuls2  28539  mulsuniflem  28540  precsexlem11  28608  twocut  28814  pw2cut2  28853  axtgcont1  28935  cgr3simp3  28990  legso  29067  hlln  29078  hltr  29081  btwnhl  29085  tghlsub  29091  mirhl  29156  mirbtwnhl  29157  opphllem4  29231  opphl  29235  hlpasch  29239  cgracgr  29330  cgraswap  29332  cgrahl  29340  cgracol  29341  inagswap  29365  inagne3  29368  dfcgrg2  29413  umgrnloopv  29689  umgredgne  29728  usgrnloopvALT  29787  frusgrnn0  30157  cusgrm1rusgr  30168  pfxwlk  30271  revwlk  30272  upgrclwlkcompim  30373  spthcycl  30397  2wlkdlem6  30525  2wlkond  30531  2trlond  30533  acycgrcycl  30758  numclwwlk2lem1  30982  numclwlk2lem2f1o  30985  tncp  31085  grpolidinv  31108  nvs  31270  nvz  31276  nvtri  31277  sspn  31343  minvecolem2  31482  minvecolem4c  31486  minvecolem4  31487  minvecolem5  31488  minvecolem6  31489  adj1  32540  cgrahlb  33052  inagbtwn  33053  cgrgptxfr  33058  inagcgratrgncol  33062  tgextahpl  33074  tgaasne  33087  eliccelico  33415  elicoelioo  33416  pmtrto1cl  33706  cyc3evpm  33757  slmdvsdir  33823  slmd0vs  33831  sdrgdvcl  33907  sdrginvcl  33908  nsgqusf1olem3  34012  mxidlmax  34036  qsdrnglem2  34066  0ringmon1p  34135  ig1pmindeg  34180  ply1degltdimlem  34300  irngss  34365  ply1annig1p  34382  minplycl  34384  algextdeglem3  34397  algextdeglem4  34398  constrsqrtcl  34457  locfinreflem  34518  cnre2csqlem  34588  sigaclci  34810  unelsiga  34812  insiga  34816  unelldsys  34837  ldsysgenld  34839  sigapildsys  34841  ldgenpisyslem1  34842  measvun  34888  cntmeas  34905  sibfima  35016  signstfveq0  35252  cgranbtwn  35344  tg5segofs  35351  bnj1018g  35639  bnj1018  35640  subfacp1lem3  36033  subfacp1lem4  36034  subfacp1lem5  36035  sconnpht2  36089  sconnpi1  36090  txsconn  36092  resconn  36097  cvmcn  36113  cvmsuni  36120  cvmsdisj  36121  cvmshmeo  36122  cvmlift2lem8  36161  cvmlift2lem13  36166  cvmliftphtlem  36168  cvmliftpht  36169  cvmlift3lem6  36175  msrf  36393  elmsta  36399  mthmpps  36433  mclsppslem  36434  ivthALT  37215  weiunfrlem  37344  weiunfr  37347  relowlssretop  38379  ibladdnc  38688  iblabsnclem  38694  ftc2nc  38713  dvasin  38715  isbndx  38809  isbnd3  38811  prdsbnd  38820  heiborlem3  38840  iccbnd  38867  rngohomadd  38996  rngohommul  38997  idladdcl  39046  idllmulcl  39047  idlrmulcl  39048  maxidlmax  39070  pridlc  39098  eqvreltr  39716  lshpnelb  40134  lshpcmp  40138  oplecon3  40349  opnoncon  40358  hlcvl  40509  dochshpncl  42534  lclkrslem1  42687  lclkrslem2  42688  fzne2d  43123  primrootsunit1  43240  primrootscoprmpow  43242  primrootlekpowne0  43248  aks6d1c1p1  43250  aks6d1c2  43273  sticksstones3  43291  aks5lem1  43329  aks5lem2  43330  aks5lem3a  43332  acongrep  44080  ntrneinex  45170  neicvgmex  45210  gneispace0nelrn  45233  cvgdvgrat  45390  binomcxplemdvbinom  45430  eliocre  46614  iccshift  46623  iccsuble  46624  icoiccdif  46629  mullimc  46721  limccog  46725  limciccioolb  46726  mullimcf  46728  limcperiod  46733  lptioo2  46736  lptioo1  46737  neglimc  46750  addlimc  46751  0ellimcdiv  46752  reclimc  46756  xlimmnfvlem1  46935  xlimpnfvlem1  46939  icccncfext  46990  cncfioobdlem  46999  ditgeqiooicc  47063  iblspltprt  47076  iblcncfioo  47081  itgiccshift  47083  itgperiod  47084  itgsbtaddcnst  47085  stoweidlem11  47114  stoweidlem31  47134  stoweidlem36  47139  stoweidlem38  47141  stoweidlem62  47165  dirkercncflem1  47206  dirkercncflem4  47209  fourierdlem26  47236  fourierdlem32  47242  fourierdlem33  47243  fourierdlem37  47247  fourierdlem42  47252  fourierdlem54  47263  fourierdlem63  47272  fourierdlem64  47273  fourierdlem65  47274  fourierdlem74  47283  fourierdlem75  47284  fourierdlem79  47288  fourierdlem81  47290  fourierdlem82  47291  fourierdlem89  47298  fourierdlem90  47299  fourierdlem91  47300  fourierdlem93  47302  fourierdlem101  47310  fourierdlem107  47316  fourierdlem109  47318  fourierdlem111  47320  salunicl  47419  saluncl  47420  hoidmv1lelem1  47694  hoidmv1lelem3  47696  hoidmvlelem1  47698  ovolval3  47750  iinhoiicclem  47776  smfpreimalt  47834  smfpreimaltf  47839  smfpreimale  47857  issmfgt  47859  smfpreimagt  47865  smfpreimage  47885  sigardiv  47964  sigarcol  47967  sharhght  47968  sigaradd  47969  cevathlem1  47970  cevathlem2  47971  cevath  47972  proththd  48792  perfectALTVlem2  48913  gpgnbgrvtx0  49265  gpgnbgrvtx1  49266  imasubc2  50361  imaf1co  50364  idfullsubc  50370  fucofulem1  50525  parcatid2  50856  parcatid  50857  rr3fv3cld  51117