Theorem simp3d 1160

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simp3bi  1163  f1dom3fv3dif  7256  f1dom3el3dif  7257  oeeui  8576  resixp  8919  domssex2  9113  cantnflem1c  9644  cantnflem1  9646  cantnflem3  9648  cantnflem4  9649  fpwwe2lem6  10609  canthnumlem  10621  canthp1lem2  10626  wununi  10679  wunpw  10680  wunpr  10682  lelttrdi  11360  ixxdisj  13378  ixxun  13379  ixxss1  13381  ixxss2  13382  ixxss12  13383  ixxub  13384  ixxlb  13385  lbioo  13394  elicore  13416  iccsupr  13460  icodisj  13494  xov1plusxeqvd  13516  intfracq  13883  fldiv  13884  seqf1olem2  14069  cjmul  15183  icco1  15581  sumtp  15790  rpnnen2lem10  16269  ruclem2  16278  ruclem3  16279  ruclem9  16284  ruclem12  16287  dvdslegcd  16552  prmdvdsbc  16775  crth  16827  eulerthlem1  16830  eulerthlem2  16831  pcpremul  16893  prmreclem2  16967  prmreclem3  16968  4sqlem13  17007  sectcan  17802  sectco  17803  sectmon  17829  monsect  17830  funcid  17917  funcco  17918  funcsect  17919  invfuc  18024  fuciso  18025  coapm  18118  catciso  18158  postr  18366  ipodrsima  18587  psref2  18616  psasym  18622  mhm0  18842  submcl  18860  submmnd  18862  eqger  19237  eqgcpbl  19241  ghmqusnsglem1  19341  ghmquskerlem1  19344  gaorber  19369  orbsta  19374  cayleyth  19476  pmtrrn2  19521  pmtrfinv  19522  pmtrfmvdn0  19523  dfod2  19625  sylow2blem1  19681  sylow2blem3  19683  dprdcntz  20071  dprddisj  20072  dprdffsupp  20077  dpjdisj  20116  ablfac1a  20132  ablfac1b  20133  lmodvsdir  20976  lmhmlin  21125  lbsind  21170  2idlcpblrng  21372  prmidl  21427  prmidlc  21435  prmidlprop  21436  qsidomlem2  21441  qsnzr  21443  evlsval3  22200  mpfind  22226  mdetunilem2  22731  mdetunilem5  22734  mdetunilem6  22735  mnfnei  23339  cnprcl  23363  lmcvg  23380  lmff  23419  lmcls  23420  lmcnp  23422  fbasssin  23954  flimfil  24087  tgpconncomp  24231  tlmtrg  24308  ustssel  24324  ustincl  24326  ustdiag  24327  ustinvel  24328  ustexhalf  24329  ustfilxp  24331  tustopn  24388  tususp  24389  imasdsf1olem  24491  xmeter  24551  xmetresbl  24555  tmstopn  24603  metustexhalf  24674  nlmnrg  24797  qdensere  24887  blcvx  24916  tgqioo  24918  icccmplem1  24941  icccmplem2  24942  reconnlem1  24945  cnmpopc  25048  iccpnfcnv  25064  phtpcer  25115  phtpcco2  25119  pcohtpy  25140  pcorev2  25148  pcophtb  25149  om1addcl  25153  pi1blem  25159  pi1cpbl  25164  pi1grplem  25169  pi1inv  25172  pi1xfrf  25173  pi1xfr  25175  pi1xfrcnvlem  25176  pi1cof  25179  pi1coghm  25181  cphreccllem  25298  cphsca  25299  cphsubrg  25300  cphsqrtcl2  25306  phclm  25352  tcphcph  25357  lmmcvg  25381  cmetcaulem  25408  lmcau  25433  bcthlem3  25446  bcthlem4  25447  minveclem4c  25545  minveclem2  25546  minveclem3b  25548  minveclem4  25552  minveclem6  25554  ivthicc  25578  ovollb2lem  25608  ovolshftlem1  25629  ovolscalem1  25633  ovolicc1  25636  ovolicc2lem2  25638  ovolicc2lem3  25639  ovolicc2lem4  25640  ovolicc2lem5  25641  ioombl1lem1  25678  dyadmaxlem  25717  volivth  25727  vitalilem2  25729  vitalilem4  25731  i1fima2  25799  itg2monolem1  25870  itgcnlem  25910  itgrevallem1  25915  itgreval  25917  itgle  25930  ibladd  25941  iblabslem  25948  itgspliticc  25957  itgsplitioo  25958  ditgcl  25978  ditgswap  25979  ditgsplitlem  25980  limcdif  25996  limcresi  26005  limcres  26006  limccnp  26011  limccnp2  26012  limcun  26015  dvlip  26113  dvlip2  26115  dveq0  26120  dvgt0lem1  26122  dvivthlem1  26128  dvcnvrelem1  26137  dvcnvre  26139  dvfsumlem2  26147  ftc1lem1  26155  ftc1lem2  26156  ftc1a  26157  ftc1lem4  26159  ftc2  26164  ftc2ditglem  26165  itgsubstlem  26168  ply1rem  26284  fta1glem2  26287  ig1pdvds  26298  plyrem  26427  fta1lem  26429  vieta1lem2  26433  aaliou3lem3  26466  pserulm  26543  psercnlem2  26545  psercnlem1  26546  psercn  26547  pserdvlem1  26548  pserdvlem2  26549  abelth2  26563  coseq00topi  26625  coseq0negpitopi  26626  cosordlem  26653  tanord1  26660  efif1olem1  26665  dvloglem  26771  efopnlem1  26779  logreclem  26885  relogbval  26895  nnlogbexp  26904  logbrec  26905  chordthmlem4  26958  quart1  26979  quartlem2  26981  quartlem3  26982  quart  26984  acosbnd  27023  atancj  27033  atanlogsublem  27038  atantan  27046  atanbndlem  27048  atans2  27054  dvatan  27058  atantayl  27060  divsqrtsumlem  27102  ftalem5  27199  basellem5  27207  ppisval  27226  chtleppi  27332  chpchtsum  27341  chpub  27342  mersenne  27349  perfectlem2  27352  dchrinv  27383  rplogsumlem2  27607  chpdifbndlem1  27675  pntibndlem2  27713  pntlema  27718  pntlemb  27719  pntlemg  27720  pntlemh  27721  pntlemr  27724  pntlemj  27725  pntlemf  27727  pntlemk  27728  pntlemo  27729  pntlemp  27732  pntleml  27733  abvcxp  27737  ostth2lem2  27756  cutsun12  27941  lesrec  27950  eqcuts3  27955  cofcut2  28073  cofcutr  28075  cofcutrtime  28078  cutmax  28085  cutmin  28086  addsproplem5  28124  addsproplem6  28125  leadds1  28140  addsuniflem  28152  addsasslem1  28154  addsasslem2  28155  negsproplem4  28182  negsproplem6  28184  negcut2  28191  negsunif  28206  mulsproplem12  28278  sltmuls1  28298  sltmuls2  28299  mulsuniflem  28300  precsexlem11  28368  twocut  28574  pw2cut2  28613  axtgcont1  28695  cgr3simp3  28749  legso  28826  hlln  28834  hltr  28837  btwnhl  28841  mirhl  28910  mirbtwnhl  28911  opphllem4  28981  opphl  28985  hlpasch  28987  cgracgr  29070  cgraswap  29072  cgrahl  29079  cgracol  29080  inagswap  29093  inagne3  29096  dfcgrg2  29115  umgrnloopv  29365  umgredgne  29404  usgrnloopvALT  29460  frusgrnn0  29830  cusgrm1rusgr  29841  upgrclwlkcompim  30039  2wlkdlem6  30189  2wlkond  30195  2trlond  30197  numclwwlk2lem1  30636  numclwlk2lem2f1o  30639  tncp  30739  grpolidinv  30762  nvs  30924  nvz  30930  nvtri  30931  sspn  30997  minvecolem2  31136  minvecolem4c  31140  minvecolem4  31141  minvecolem5  31142  minvecolem6  31143  adj1  32194  eliccelico  33034  elicoelioo  33035  pmtrto1cl  33332  cyc3evpm  33383  slmdvsdir  33449  slmd0vs  33457  sdrgdvcl  33535  sdrginvcl  33536  nsgqusf1olem3  33640  mxidlmax  33665  qsdrnglem2  33695  0ringmon1p  33764  ig1pmindeg  33809  ply1degltdimlem  33929  irngss  33994  ply1annig1p  34011  minplycl  34013  algextdeglem3  34026  algextdeglem4  34027  constrsqrtcl  34086  locfinreflem  34147  cnre2csqlem  34217  sigaclci  34439  unelsiga  34441  insiga  34444  unelldsys  34465  ldsysgenld  34467  sigapildsys  34469  ldgenpisyslem1  34470  measvun  34516  cntmeas  34533  sibfima  34645  signstfveq0  34881  cgranbtwn  34973  tg5segofs  34980  bnj1018g  35268  bnj1018  35269  pfxwlk  35487  revwlk  35488  spthcycl  35492  acycgrcycl  35510  subfacp1lem3  35545  subfacp1lem4  35546  subfacp1lem5  35547  sconnpht2  35601  sconnpi1  35602  txsconn  35604  resconn  35609  cvmcn  35625  cvmsuni  35632  cvmsdisj  35633  cvmshmeo  35634  cvmlift2lem8  35673  cvmlift2lem13  35678  cvmliftphtlem  35680  cvmliftpht  35681  cvmlift3lem6  35687  msrf  35905  elmsta  35911  mthmpps  35945  mclsppslem  35946  ivthALT  36708  weiunfrlem  36837  weiunfr  36840  relowlssretop  37869  ibladdnc  38188  iblabsnclem  38194  ftc2nc  38213  dvasin  38215  isbndx  38293  isbnd3  38295  prdsbnd  38304  heiborlem3  38324  iccbnd  38351  rngohomadd  38480  rngohommul  38481  idladdcl  38530  idllmulcl  38531  idlrmulcl  38532  maxidlmax  38554  pridlc  38582  eqvreltr  39202  lshpnelb  39620  lshpcmp  39624  oplecon3  39835  opnoncon  39844  hlcvl  39995  dochshpncl  42020  lclkrslem1  42173  lclkrslem2  42174  fzne2d  42609  primrootsunit1  42726  primrootscoprmpow  42728  primrootlekpowne0  42734  aks6d1c1p1  42736  aks6d1c2  42759  sticksstones3  42777  aks5lem1  42815  aks5lem2  42816  aks5lem3a  42818  flt4lem5f  43251  flt4lem7  43253  nna4b4nsq  43254  acongrep  43569  ntrneinex  44665  neicvgmex  44705  gneispace0nelrn  44728  cvgdvgrat  44887  binomcxplemdvbinom  44927  eliocre  46083  iccshift  46092  iccsuble  46093  icoiccdif  46098  mullimc  46190  limccog  46194  limciccioolb  46195  mullimcf  46197  limcperiod  46202  lptioo2  46205  lptioo1  46206  neglimc  46219  addlimc  46220  0ellimcdiv  46221  reclimc  46225  xlimmnfvlem1  46404  xlimpnfvlem1  46408  icccncfext  46459  cncfioobdlem  46468  ditgeqiooicc  46532  iblspltprt  46545  iblcncfioo  46550  itgiccshift  46552  itgperiod  46553  itgsbtaddcnst  46554  stoweidlem11  46583  stoweidlem31  46603  stoweidlem36  46608  stoweidlem38  46610  stoweidlem62  46634  dirkercncflem1  46675  dirkercncflem4  46678  fourierdlem26  46705  fourierdlem32  46711  fourierdlem33  46712  fourierdlem37  46716  fourierdlem42  46721  fourierdlem54  46732  fourierdlem63  46741  fourierdlem64  46742  fourierdlem65  46743  fourierdlem74  46752  fourierdlem75  46753  fourierdlem79  46757  fourierdlem81  46759  fourierdlem82  46760  fourierdlem89  46767  fourierdlem90  46768  fourierdlem91  46769  fourierdlem93  46771  fourierdlem101  46779  fourierdlem107  46785  fourierdlem109  46787  fourierdlem111  46789  salunicl  46888  saluncl  46889  hoidmv1lelem1  47163  hoidmv1lelem3  47165  hoidmvlelem1  47167  ovolval3  47219  iinhoiicclem  47245  smfpreimalt  47303  smfpreimaltf  47308  smfpreimale  47326  issmfgt  47328  smfpreimagt  47334  smfpreimage  47354  sigardiv  47433  sigarcol  47436  sharhght  47437  sigaradd  47438  cevathlem1  47439  cevathlem2  47440  cevath  47441  proththd  48221  perfectALTVlem2  48342  gpgnbgrvtx0  48694  gpgnbgrvtx1  48695  imasubc2  49781  imaf1co  49784  idfullsubc  49790  fucofulem1  49939