Theorem simp1d 1142

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp1bi  1145  f1dom3fv3dif  7246  f1dom3el3dif  7247  f1prex  7262  oeeui  8569  oeeu  8570  domssex2  9107  domssex  9108  cantnflem1a  9645  cantnflem1b  9646  cantnflem1c  9647  cantnflem1d  9648  cantnflem1  9649  cantnflem3  9651  cantnflem4  9652  fpwwe2lem6  10596  canthnumlem  10608  canthp1lem2  10613  wuntr  10665  lelttrdi  11343  supmul1  12159  supmullem1  12160  supmullem2  12161  supmul  12162  ixxdisj  13328  ixxun  13329  ixxss1  13331  ixxss2  13332  ixxss12  13333  ixxub  13334  ixxlb  13335  iccss2  13385  iocssre  13395  icossre  13396  iccssre  13397  icodisj  13444  iccf1o  13464  xov1plusxeqvd  13466  fzen  13509  intfracq  13828  fldiv  13829  remul  15102  01sqrexlem6  15220  resqrtth  15228  sqrtth  15338  ruclem6  16210  ruclem9  16213  ruclem12  16216  gcdn0cl  16479  crth  16755  phimullem  16756  eulerthlem1  16758  eulerthlem2  16759  pcpremul  16821  prmreclem3  16896  sectcan  17724  sectco  17725  sectmon  17751  monsect  17752  funcf1  17835  funcsect  17841  invfuc  17946  coapm  18040  catciso  18080  psrel  18535  pstr  18543  mhmf  18723  submss  18743  eqger  19117  eqgcpbl  19121  gaorber  19247  orbstafun  19250  cayleyth  19352  dprdgrp  19944  dprdff  19951  ablfac1a  20008  ablfac1b  20009  lmodvscl  20791  lbsss  20991  2idlcpblrng  21188  mpfind  22021  mdetunilem2  22507  mdetunilem5  22510  mdetunilem6  22511  chfacfisfcpmat  22749  cnptop1  23136  lmfpm  23189  lmff  23195  lmcnp  23198  flimtop  23859  tlmtmd  24081  ustssxp  24099  ustdiag  24103  ustfilxp  24107  ustbas2  24120  tusbas  24162  imasdsf1olem  24268  xmeter  24328  tmsbas  24378  metustexhalf  24451  nlmngp  24572  qdensere  24664  blcvx  24693  tgqioo  24695  icccmplem2  24719  reconnlem1  24722  cnmpopc  24829  icoopnst  24843  iocopnst  24844  iccpnfcnv  24849  phtpcer  24901  phtpcco2  24906  pcohtpylem  24926  pcohtpy  24927  pcopt  24929  pcopt2  24930  pcorevlem  24933  pcorev2  24935  pcophtb  24936  om1addcl  24940  pi1grplem  24956  pi1inv  24959  pi1xfrf  24960  pi1xfr  24962  pi1xfrcnvlem  24963  pi1xfrcnv  24964  pi1cof  24966  pi1coghm  24968  cphphl  25078  cphreccllem  25085  cphsqrtcl2  25093  phclm  25139  tcphcph  25144  lmcau  25220  bcthlem4  25234  minveclem4c  25332  minveclem2  25333  minveclem3b  25335  minveclem4  25339  minveclem6  25341  ivthicc  25366  ovolfsval  25378  ovollb2lem  25396  ovolshftlem1  25417  ovolscalem1  25421  ovolicc2lem2  25426  ovolicc2lem5  25429  ovolicopnf  25432  ioombl1lem1  25466  ioombl1lem3  25468  ioombl1lem4  25469  uniioovol  25487  uniioombllem2a  25490  uniioombllem2  25491  uniioombllem3a  25492  uniioombllem3  25493  uniioombllem4  25494  uniioombllem6  25496  vitalilem2  25517  vitalilem3  25518  vitalilem4  25519  i1ff  25584  itg2monolem1  25658  itgreval  25705  ibladd  25729  iblabslem  25736  itgspliticc  25745  itgsplitioo  25746  ditgcl  25766  ditgswap  25767  ditgsplitlem  25768  ditgsplit  25769  limcresi  25793  dvlip2  25907  dveq0  25912  dvcnvre  25931  dvfsumlem2  25940  dvfsumlem2OLD  25941  ftc1a  25951  ply1rem  26078  facth1  26079  fta1glem1  26080  fta1glem2  26081  ig1pcl  26091  ig1pdvds  26092  plyrem  26220  facth  26221  vieta1lem1  26225  vieta1lem2  26226  aaliou3lem3  26259  aaliou3lem7  26264  pserulm  26338  psercnlem2  26341  psercn  26343  pserdvlem1  26344  pserdvlem2  26345  pserdv  26346  abelth2  26359  coseq00topi  26418  coseq0negpitopi  26419  cosordlem  26446  efif1olem1  26458  dvloglem  26564  loglesqrt  26678  relogbval  26689  nnlogbexp  26698  logbrec  26699  quart1  26773  quartlem2  26775  quartlem3  26776  quartlem4  26777  quart  26778  asinsinlem  26808  atanlogsublem  26832  atans2  26848  dvatan  26852  rlimcnp2  26883  divsqrtsumlem  26897  ftalem5  26994  ftalem7  26996  basellem4  27001  basellem5  27002  perfectlem2  27148  dchrinv  27179  chpdifbndlem1  27471  pntibndlem2  27509  pntlema  27514  pntlemb  27515  pntlemg  27516  pntlemh  27517  pntlemn  27518  pntlemq  27519  pntlemr  27520  pntlemj  27521  pntlemf  27523  pntlemk  27524  pntlemo  27525  pntlemp  27528  pntleml  27529  abvcxp  27533  scutcl  27721  scutun12  27729  sltrec  27739  addsproplem6  27888  addsprop  27890  addscld  27894  negsproplem6  27946  negsprop  27948  mulsproplem11  28036  mulsproplem12  28037  axtgbtwnid  28400  cgr3simp1  28454  hlne1  28539  hltr  28544  btwnhl  28548  mirhl  28613  opphllem4  28684  hlpasch  28690  inagswap  28775  inagne1  28776  dfcgrg2  28797  wlkf  29549  wlk1ewlk  29575  2wlkdlem6  29868  2wlkond  29874  2trlond  29876  grpofo  30435  vcablo  30505  nvvc  30551  sspba  30663  sspg  30664  minvecolem2  30811  minvecolem4c  30815  minvecolem4  30816  minvecolem5  30817  minvecolem6  30818  eleigveccl  31895  tpssad  32475  xrofsup  32697  eliccelico  32707  elicoelioo  32708  cyc3evpm  33114  slmdvscl  33174  slmdvsass  33177  imaslmod  33331  prmidlidl  33422  mxidlidl  33441  0ringmon1p  33533  irngss  33689  algextdeglem1  33714  constrsqrtcl  33776  baselsiga  34112  insiga  34134  ldsysgenld  34157  sigapildsys  34159  ldgenpisyslem1  34160  measfrge0  34200  sibfmbl  34333  eulerpartlemt  34369  eulerpartlemmf  34373  probfinmeasbALTV  34427  tg5segofs  34671  pfxwlk  35118  revwlk  35119  subgrwlk  35126  subfacp1lem2a  35174  subfacp1lem2b  35175  subfacp1lem3  35176  subfacp1lem4  35177  subfacp1lem5  35178  sconnpht2  35232  sconnpi1  35233  cvxsconn  35237  cvmlift2lem3  35299  cvmlift2lem5  35301  cvmlift2lem6  35302  cvmlift2lem7  35303  cvmlift2lem12  35308  cvmliftphtlem  35311  cvmliftpht  35312  cvmlift3lem2  35314  cvmlift3lem4  35316  cvmlift3lem5  35317  cvmlift3lem6  35318  msrf  35536  elmsta  35542  mthmpps  35576  mclsppslem  35577  mclspps  35578  weiunfrlem  36459  weiunpo  36460  weiunso  36461  weiunfr  36462  weiunse  36463  iblabsnclem  37684  dvasin  37705  isbnd3  37785  heiborlem3  37814  iccbnd  37841  rngohomf  37967  idlss  38017  lshplss  38981  opoccl  39194  opococ  39195  oplecon3  39199  hloml  39357  lclkrslem1  41538  lclkrslem2  41539  dvrelog2  42059  dvrelog3  42060  aks4d1p1p5  42070  primrootsunit1  42092  primrootscoprmpow  42094  primrootscoprbij  42097  primrootspoweq0  42101  aks6d1c1p2  42104  aks6d1c1p3  42105  aks6d1c1p4  42106  aks6d1c1p5  42107  aks6d1c1p7  42108  aks6d1c1p6  42109  aks6d1c1p8  42110  aks6d1c2lem3  42121  aks6d1c2lem4  42122  aks6d1c2  42125  aks6d1c6lem2  42166  aks6d1c6lem3  42167  aks6d1c6lem4  42168  aks6d1c6isolem1  42169  aks6d1c6isolem2  42170  aks6d1c6lem5  42172  aks5lem1  42181  aks5lem2  42182  aks5lem3a  42184  evlsval3  42554  flt4lem5f  42652  flt4lem7  42654  nna4b4nsq  42655  eliccre  45510  eliocre  45514  icoiccdif  45529  limccog  45625  lptioo1  45637  cncfiooicclem1  45898  ditgeqiooicc  45965  stoweidlem30  46035  stoweidlem31  46036  stoweidlem38  46043  stoweidlem44  46049  fourierdlem26  46138  fourierdlem32  46144  fourierdlem33  46145  fourierdlem37  46149  fourierdlem42  46154  fourierdlem54  46165  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem69  46180  fourierdlem79  46190  fourierdlem82  46193  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem111  46222  0sal  46325  hoidmv1lelem3  46598  smfdmss  46738  sigardiv  46866  sigarcol  46869  sharhght  46870  sigaradd  46871  cevathlem1  46872  cevathlem2  46873  cevath  46874  proththd  47619  perfectALTVlem2  47727  isuspgrim0  47898  gpgnbgrvtx0  48069  gpgnbgrvtx1  48070  itsclc0yqsol  48757  imaf1hom  49101