Theorem simp1d 1143

Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
3simp1d.1	⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp1d	⊢ (𝜑 → 𝜓)

Proof of Theorem simp1d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp1 1137	. 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simp1bi  1146  f1dom3fv3dif  7216  f1dom3el3dif  7217  f1prex  7232  oeeui  8531  oeeu  8532  domssex2  9068  domssex  9069  cantnflem1a  9597  cantnflem1b  9598  cantnflem1c  9599  cantnflem1d  9600  cantnflem1  9601  cantnflem3  9603  cantnflem4  9604  fpwwe2lem6  10550  canthnumlem  10562  canthp1lem2  10567  wuntr  10619  lelttrdi  11299  supmul1  12116  supmullem1  12117  supmullem2  12118  supmul  12119  ixxdisj  13304  ixxun  13305  ixxss1  13307  ixxss2  13308  ixxss12  13309  ixxub  13310  ixxlb  13311  iccss2  13361  iocssre  13371  icossre  13372  iccssre  13373  icodisj  13420  iccf1o  13440  xov1plusxeqvd  13442  fzen  13486  intfracq  13809  fldiv  13810  remul  15082  01sqrexlem6  15200  resqrtth  15208  sqrtth  15318  ruclem6  16193  ruclem9  16196  ruclem12  16199  gcdn0cl  16462  crth  16739  phimullem  16740  eulerthlem1  16742  eulerthlem2  16743  pcpremul  16805  prmreclem3  16880  sectcan  17713  sectco  17714  sectmon  17740  monsect  17741  funcf1  17824  funcsect  17830  invfuc  17935  coapm  18029  catciso  18069  psrel  18526  pstr  18534  mhmf  18748  submss  18768  eqger  19144  eqgcpbl  19148  gaorber  19274  orbstafun  19277  cayleyth  19381  dprdgrp  19973  dprdff  19980  ablfac1a  20037  ablfac1b  20038  lmodvscl  20864  lbsss  21064  2idlcpblrng  21261  evlsval3  22077  mpfind  22103  mdetunilem2  22588  mdetunilem5  22591  mdetunilem6  22592  chfacfisfcpmat  22830  cnptop1  23217  lmfpm  23270  lmff  23276  lmcnp  23279  flimtop  23940  tlmtmd  24162  ustssxp  24180  ustdiag  24184  ustfilxp  24188  ustbas2  24200  tusbas  24242  imasdsf1olem  24348  xmeter  24408  tmsbas  24458  metustexhalf  24531  nlmngp  24652  qdensere  24744  blcvx  24773  tgqioo  24775  icccmplem2  24799  reconnlem1  24802  cnmpopc  24905  icoopnst  24916  iocopnst  24917  iccpnfcnv  24921  phtpcer  24972  phtpcco2  24976  pcohtpylem  24996  pcohtpy  24997  pcopt  24999  pcopt2  25000  pcorevlem  25003  pcorev2  25005  pcophtb  25006  om1addcl  25010  pi1grplem  25026  pi1inv  25029  pi1xfrf  25030  pi1xfr  25032  pi1xfrcnvlem  25033  pi1xfrcnv  25034  pi1cof  25036  pi1coghm  25038  cphphl  25148  cphreccllem  25155  cphsqrtcl2  25163  phclm  25209  tcphcph  25214  lmcau  25290  bcthlem4  25304  minveclem4c  25402  minveclem2  25403  minveclem3b  25405  minveclem4  25409  minveclem6  25411  ivthicc  25435  ovolfsval  25447  ovollb2lem  25465  ovolshftlem1  25486  ovolscalem1  25490  ovolicc2lem2  25495  ovolicc2lem5  25498  ovolicopnf  25501  ioombl1lem1  25535  ioombl1lem3  25537  ioombl1lem4  25538  uniioovol  25556  uniioombllem2a  25559  uniioombllem2  25560  uniioombllem3a  25561  uniioombllem3  25562  uniioombllem4  25563  uniioombllem6  25565  vitalilem2  25586  vitalilem3  25587  vitalilem4  25588  i1ff  25653  itg2monolem1  25727  itgreval  25774  ibladd  25798  iblabslem  25805  itgspliticc  25814  itgsplitioo  25815  ditgcl  25835  ditgswap  25836  ditgsplitlem  25837  ditgsplit  25838  limcresi  25862  dvlip2  25972  dveq0  25977  dvcnvre  25996  dvfsumlem2  26004  ftc1a  26014  ply1rem  26141  facth1  26142  fta1glem1  26143  fta1glem2  26144  ig1pcl  26154  ig1pdvds  26155  plyrem  26282  facth  26283  vieta1lem1  26287  vieta1lem2  26288  aaliou3lem3  26321  aaliou3lem7  26326  pserulm  26400  psercnlem2  26402  psercn  26404  pserdvlem1  26405  pserdvlem2  26406  pserdv  26407  abelth2  26420  coseq00topi  26479  coseq0negpitopi  26480  cosordlem  26507  efif1olem1  26519  dvloglem  26625  loglesqrt  26738  relogbval  26749  nnlogbexp  26758  logbrec  26759  quart1  26833  quartlem2  26835  quartlem3  26836  quartlem4  26837  quart  26838  asinsinlem  26868  atanlogsublem  26892  atans2  26908  dvatan  26912  rlimcnp2  26943  divsqrtsumlem  26957  ftalem5  27054  ftalem7  27056  basellem4  27061  basellem5  27062  perfectlem2  27207  dchrinv  27238  chpdifbndlem1  27530  pntibndlem2  27568  pntlema  27573  pntlemb  27574  pntlemg  27575  pntlemh  27576  pntlemn  27577  pntlemq  27578  pntlemr  27579  pntlemj  27580  pntlemf  27582  pntlemk  27583  pntlemo  27584  pntlemp  27587  pntleml  27588  abvcxp  27592  cutscl  27788  cutsun12  27796  ltsrec  27807  addsproplem6  27980  addsprop  27982  addscld  27986  negsproplem6  28039  negsprop  28041  mulsproplem11  28132  mulsproplem12  28133  axtgbtwnid  28548  cgr3simp1  28602  hlne1  28687  hltr  28692  btwnhl  28696  mirhl  28761  opphllem4  28832  hlpasch  28838  inagswap  28923  inagne1  28924  dfcgrg2  28945  wlkf  29698  wlk1ewlk  29723  2wlkdlem6  30014  2wlkond  30020  2trlond  30022  grpofo  30585  vcablo  30655  nvvc  30701  sspba  30813  sspg  30814  minvecolem2  30961  minvecolem4c  30965  minvecolem4  30966  minvecolem5  30967  minvecolem6  30968  eleigveccl  32045  tpssad  32624  xrofsup  32855  eliccelico  32865  elicoelioo  32866  cyc3evpm  33226  slmdvscl  33290  slmdvsass  33293  imaslmod  33428  prmidlidl  33519  mxidlidl  33538  0ringmon1p  33632  irngss  33847  algextdeglem1  33877  constrsqrtcl  33939  baselsiga  34275  insiga  34297  ldsysgenld  34320  sigapildsys  34322  ldgenpisyslem1  34323  measfrge0  34363  sibfmbl  34495  eulerpartlemt  34531  eulerpartlemmf  34535  probfinmeasbALTV  34589  tg5segofs  34833  pfxwlk  35322  revwlk  35323  subgrwlk  35330  subfacp1lem2a  35378  subfacp1lem2b  35379  subfacp1lem3  35380  subfacp1lem4  35381  subfacp1lem5  35382  sconnpht2  35436  sconnpi1  35437  cvxsconn  35441  cvmlift2lem3  35503  cvmlift2lem5  35505  cvmlift2lem6  35506  cvmlift2lem7  35507  cvmlift2lem12  35512  cvmliftphtlem  35515  cvmliftpht  35516  cvmlift3lem2  35518  cvmlift3lem4  35520  cvmlift3lem5  35521  cvmlift3lem6  35522  msrf  35740  elmsta  35746  mthmpps  35780  mclsppslem  35781  mclspps  35782  weiunfrlem  36662  weiunpo  36663  weiunso  36664  weiunfr  36665  weiunse  36666  iblabsnclem  38018  dvasin  38039  isbnd3  38119  heiborlem3  38148  iccbnd  38175  rngohomf  38301  idlss  38351  lshplss  39441  opoccl  39654  opococ  39655  oplecon3  39659  hloml  39817  lclkrslem1  41997  lclkrslem2  41998  dvrelog2  42517  dvrelog3  42518  aks4d1p1p5  42528  primrootsunit1  42550  primrootscoprmpow  42552  primrootscoprbij  42555  primrootspoweq0  42559  aks6d1c1p2  42562  aks6d1c1p3  42563  aks6d1c1p4  42564  aks6d1c1p5  42565  aks6d1c1p7  42566  aks6d1c1p6  42567  aks6d1c1p8  42568  aks6d1c2lem3  42579  aks6d1c2lem4  42580  aks6d1c2  42583  aks6d1c6lem2  42624  aks6d1c6lem3  42625  aks6d1c6lem4  42626  aks6d1c6isolem1  42627  aks6d1c6isolem2  42628  aks6d1c6lem5  42630  aks5lem1  42639  aks5lem2  42640  aks5lem3a  42642  flt4lem5f  43104  flt4lem7  43106  nna4b4nsq  43107  eliccre  45953  eliocre  45957  icoiccdif  45972  limccog  46068  lptioo1  46080  cncfiooicclem1  46339  ditgeqiooicc  46406  stoweidlem30  46476  stoweidlem31  46477  stoweidlem38  46484  stoweidlem44  46490  fourierdlem26  46579  fourierdlem32  46585  fourierdlem33  46586  fourierdlem37  46590  fourierdlem42  46595  fourierdlem54  46606  fourierdlem63  46615  fourierdlem64  46616  fourierdlem65  46617  fourierdlem69  46621  fourierdlem79  46631  fourierdlem82  46634  fourierdlem89  46641  fourierdlem90  46642  fourierdlem91  46643  fourierdlem111  46663  0sal  46766  hoidmv1lelem3  47039  smfdmss  47179  sigardiv  47307  sigarcol  47310  sharhght  47311  sigaradd  47312  cevathlem1  47313  cevathlem2  47314  cevath  47315  nthrucw  47332  proththd  48089  perfectALTVlem2  48210  isuspgrim0  48382  gpgnbgrvtx0  48562  gpgnbgrvtx1  48563  itsclc0yqsol  49252  imaf1hom  49595