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  7295  f1dom3el3dif  7296  oeeui  8639  resixp  8989  domssex2  9184  cantnflem1c  9715  cantnflem1  9717  cantnflem3  9719  cantnflem4  9720  fpwwe2lem6  10748  canthnumlem  10760  canthp1lem2  10765  wununi  10818  wunpw  10819  wunpr  10821  lelttrdi  11499  ixxdisj  13518  ixxun  13519  ixxss1  13521  ixxss2  13522  ixxss12  13523  ixxub  13524  ixxlb  13525  lbioo  13534  elicore  13556  iccsupr  13600  icodisj  13634  xov1plusxeqvd  13656  intfracq  14026  fldiv  14027  seqf1olem2  14212  cjmul  15338  icco1  15736  sumtp  15944  rpnnen2lem10  16420  ruclem2  16429  ruclem3  16430  ruclem9  16435  ruclem12  16438  dvdslegcd  16703  prmdvdsbc  16931  crth  16984  eulerthlem1  16987  eulerthlem2  16988  pcpremul  17050  prmreclem2  17124  prmreclem3  17125  4sqlem13  17164  sectcan  17959  sectco  17960  sectmon  17986  monsect  17987  funcid  18074  funcco  18075  funcsect  18076  invfuc  18181  fuciso  18182  coapm  18275  catciso  18315  postr  18523  ipodrsima  18744  psref2  18773  psasym  18779  mhm0  19018  submcl  19036  submmnd  19038  eqger  19419  eqgcpbl  19423  ghmqusnsglem1  19524  ghmquskerlem1  19527  gaorber  19552  orbsta  19557  cayleyth  19659  pmtrrn2  19704  pmtrfinv  19705  pmtrfmvdn0  19706  dfod2  19808  sylow2blem1  19864  sylow2blem3  19866  dprdcntz  20254  dprddisj  20255  dprdffsupp  20260  dpjdisj  20299  ablfac1a  20315  ablfac1b  20316  lmodvsdir  21191  lmhmlin  21340  lbsind  21385  2idlcpblrng  21595  prmidl  21651  prmidlc  21659  prmidlprop  21662  qsidomlem2  21667  qsnzr  21669  evlsval3  22428  mpfind  22454  mdetunilem2  22958  mdetunilem5  22961  mdetunilem6  22962  mnfnei  23569  cnprcl  23593  lmcvg  23610  lmff  23649  lmcls  23650  lmcnp  23652  fbasssin  24185  flimfil  24318  tgpconncomp  24462  tlmtrg  24539  ustssel  24555  ustincl  24557  ustdiag  24558  ustinvel  24559  ustexhalf  24560  ustfilxp  24562  tustopn  24619  tususp  24620  imasdsf1olem  24722  xmeter  24782  xmetresbl  24786  tmstopn  24834  metustexhalf  24905  nlmnrg  25028  qdensere  25118  blcvx  25147  tgqioo  25149  icccmplem1  25172  icccmplem2  25173  reconnlem1  25176  cnmpopc  25279  iccpnfcnv  25295  phtpcer  25346  phtpcco2  25350  pcohtpy  25371  pcorev2  25379  pcophtb  25380  om1addcl  25384  pi1blem  25390  pi1cpbl  25395  pi1grplem  25400  pi1inv  25403  pi1xfrf  25404  pi1xfr  25406  pi1xfrcnvlem  25407  pi1cof  25410  pi1coghm  25412  cphreccllem  25529  cphsca  25530  cphsubrg  25531  cphsqrtcl2  25537  phclm  25583  tcphcph  25588  lmmcvg  25612  cmetcaulem  25639  lmcau  25664  bcthlem3  25677  bcthlem4  25678  minveclem4c  25776  minveclem2  25777  minveclem3b  25779  minveclem4  25783  minveclem6  25785  ivthicc  25809  ovollb2lem  25839  ovolshftlem1  25860  ovolscalem1  25864  ovolicc1  25867  ovolicc2lem2  25869  ovolicc2lem3  25870  ovolicc2lem4  25871  ovolicc2lem5  25872  ioombl1lem1  25909  dyadmaxlem  25948  volivth  25958  vitalilem2  25960  vitalilem4  25962  i1fima2  26030  itg2monolem1  26101  itgcnlem  26140  itgrevallem1  26145  itgreval  26147  itgle  26160  ibladd  26171  iblabslem  26178  itgspliticc  26187  itgsplitioo  26188  ditgcl  26208  ditgswap  26209  ditgsplitlem  26210  limcdif  26226  limcresi  26235  limcres  26236  limccnp  26241  limccnp2  26242  limcun  26245  dvlip  26343  dvlip2  26345  dveq0  26350  dvgt0lem1  26352  dvivthlem1  26358  dvcnvrelem1  26367  dvcnvre  26369  dvfsumlem2  26377  ftc1lem1  26385  ftc1lem2  26386  ftc1a  26387  ftc1lem4  26389  ftc2  26394  ftc2ditglem  26395  itgsubstlem  26398  ply1rem  26514  fta1glem2  26517  ig1pdvds  26528  plyrem  26656  fta1lem  26658  vieta1lem2  26664  aaliou3lem3  26701  pserulm  26779  psercnlem2  26781  psercnlem1  26782  psercn  26783  pserdvlem1  26784  pserdvlem2  26785  abelth2  26799  coseq00topi  26861  coseq0negpitopi  26862  cosordlem  26888  tanord1  26895  efif1olem1  26900  dvloglem  27006  efopnlem1  27014  logreclem  27120  relogbval  27130  nnlogbexp  27139  logbrec  27140  chordthmlem4  27193  quart1  27214  quartlem2  27216  quartlem3  27217  quart  27219  acosbnd  27258  atancj  27268  atanlogsublem  27273  atantan  27281  atanbndlem  27283  atans2  27289  dvatan  27293  atantayl  27295  divsqrtsumlem  27337  ftalem5  27434  basellem5  27442  ppisval  27461  chtleppi  27567  chpchtsum  27576  chpub  27577  mersenne  27584  perfectlem2  27587  dchrinv  27618  rplogsumlem2  27842  chpdifbndlem1  27910  pntibndlem2  27948  pntlema  27953  pntlemb  27954  pntlemg  27955  pntlemh  27956  pntlemr  27959  pntlemj  27960  pntlemf  27962  pntlemk  27963  pntlemo  27964  pntlemp  27967  pntleml  27968  abvcxp  27972  ostth2lem2  27991  flt4lem5f  28017  flt4lem7  28019  nna4b4nsq  28020  cutsun12  28206  lesrec  28215  eqcuts3  28220  cofcut2  28338  cofcutr  28340  cofcutrtime  28343  cutmax  28350  cutmin  28351  addsproplem5  28389  addsproplem6  28390  leadds1  28405  addsuniflem  28417  addsasslem1  28419  addsasslem2  28420  negsproplem4  28447  negsproplem6  28449  negcut2  28456  negsunif  28471  mulsproplem12  28543  sltmuls1  28563  sltmuls2  28564  mulsuniflem  28565  precsexlem11  28633  twocut  28839  pw2cut2  28878  axtgcont1  28960  cgr3simp3  29015  legso  29092  hlln  29103  hltr  29106  btwnhl  29110  tghlsub  29116  mirhl  29181  mirbtwnhl  29182  opphllem4  29256  opphl  29260  hlpasch  29264  cgracgr  29355  cgraswap  29357  cgrahl  29365  cgracol  29366  inagswap  29390  inagne3  29393  dfcgrg2  29438  umgrnloopv  29714  umgredgne  29753  usgrnloopvALT  29812  frusgrnn0  30182  cusgrm1rusgr  30193  pfxwlk  30296  revwlk  30297  upgrclwlkcompim  30398  spthcycl  30422  2wlkdlem6  30550  2wlkond  30556  2trlond  30558  acycgrcycl  30783  numclwwlk2lem1  31007  numclwlk2lem2f1o  31010  tncp  31110  grpolidinv  31133  nvs  31295  nvz  31301  nvtri  31302  sspn  31368  minvecolem2  31507  minvecolem4c  31511  minvecolem4  31512  minvecolem5  31513  minvecolem6  31514  adj1  32565  cgrahlb  33077  inagbtwn  33078  cgrgptxfr  33083  inagcgratrgncol  33087  tgextahpl  33099  tgaasne  33112  eliccelico  33439  elicoelioo  33440  pmtrto1cl  33730  cyc3evpm  33781  slmdvsdir  33847  slmd0vs  33855  sdrgdvcl  33931  sdrginvcl  33932  nsgqusf1olem3  34036  mxidlmax  34060  qsdrnglem2  34090  0ringmon1p  34159  ig1pmindeg  34204  ply1degltdimlem  34324  irngss  34389  ply1annig1p  34406  minplycl  34408  algextdeglem3  34421  algextdeglem4  34422  constrsqrtcl  34481  locfinreflem  34542  cnre2csqlem  34612  sigaclci  34834  unelsiga  34836  insiga  34840  unelldsys  34861  ldsysgenld  34863  sigapildsys  34865  ldgenpisyslem1  34866  measvun  34912  cntmeas  34929  sibfima  35040  signstfveq0  35276  cgranbtwn  35368  tg5segofs  35375  bnj1018g  35663  bnj1018  35664  dfk32  36014  subfacp1lem3  36114  subfacp1lem4  36115  subfacp1lem5  36116  sconnpht2  36170  sconnpi1  36171  txsconn  36173  resconn  36178  cvmcn  36194  cvmsuni  36201  cvmsdisj  36202  cvmshmeo  36203  cvmlift2lem8  36242  cvmlift2lem13  36247  cvmliftphtlem  36249  cvmliftpht  36250  cvmlift3lem6  36256  msrf  36474  elmsta  36480  mthmpps  36514  mclsppslem  36515  ivthALT  37301  weiunfrlem  37430  weiunfr  37433  relowlssretop  38478  ibladdnc  38787  iblabsnclem  38793  ftc2nc  38812  dvasin  38814  isbndx  38908  isbnd3  38910  prdsbnd  38919  heiborlem3  38939  iccbnd  38966  rngohomadd  39095  rngohommul  39096  idladdcl  39145  idllmulcl  39146  idlrmulcl  39147  maxidlmax  39169  pridlc  39197  eqvreltr  39815  lshpnelb  40233  lshpcmp  40237  oplecon3  40448  opnoncon  40457  hlcvl  40608  dochshpncl  42633  lclkrslem1  42786  lclkrslem2  42787  fzne2d  43222  primrootsunit1  43339  primrootscoprmpow  43341  primrootlekpowne0  43347  aks6d1c1p1  43349  aks6d1c2  43372  sticksstones3  43390  aks5lem1  43428  aks5lem2  43429  aks5lem3a  43431  acongrep  44180  ntrneinex  45269  neicvgmex  45309  gneispace0nelrn  45332  cvgdvgrat  45489  binomcxplemdvbinom  45529  eliocre  46726  iccshift  46735  iccsuble  46736  icoiccdif  46741  mullimc  46833  limccog  46837  limciccioolb  46838  mullimcf  46840  limcperiod  46845  lptioo2  46848  lptioo1  46849  neglimc  46862  addlimc  46863  0ellimcdiv  46864  reclimc  46868  xlimmnfvlem1  47047  xlimpnfvlem1  47051  icccncfext  47102  cncfioobdlem  47111  ditgeqiooicc  47175  iblspltprt  47188  iblcncfioo  47193  itgiccshift  47195  itgperiod  47196  itgsbtaddcnst  47197  stoweidlem11  47226  stoweidlem31  47246  stoweidlem36  47251  stoweidlem38  47253  stoweidlem62  47277  dirkercncflem1  47318  dirkercncflem4  47321  fourierdlem26  47348  fourierdlem32  47354  fourierdlem33  47355  fourierdlem37  47359  fourierdlem42  47364  fourierdlem54  47375  fourierdlem63  47384  fourierdlem64  47385  fourierdlem65  47386  fourierdlem74  47395  fourierdlem75  47396  fourierdlem79  47400  fourierdlem81  47402  fourierdlem82  47403  fourierdlem89  47410  fourierdlem90  47411  fourierdlem91  47412  fourierdlem93  47414  fourierdlem101  47422  fourierdlem107  47428  fourierdlem109  47430  fourierdlem111  47432  salunicl  47531  saluncl  47532  hoidmv1lelem1  47806  hoidmv1lelem3  47808  hoidmvlelem1  47810  ovolval3  47862  iinhoiicclem  47888  smfpreimalt  47946  smfpreimaltf  47951  smfpreimale  47969  issmfgt  47971  smfpreimagt  47977  smfpreimage  47997  sigardiv  48076  sigarcol  48079  sharhght  48080  sigaradd  48081  cevathlem1  48082  cevathlem2  48083  cevath  48084  proththd  48904  perfectALTVlem2  49025  gpgnbgrvtx0  49377  gpgnbgrvtx1  49378  imasubc2  50473  imaf1co  50476  idfullsubc  50482  fucofulem1  50637  parcatid2  50968  parcatid  50969  rr3fv3cld  51229