Theorem simp1d 1141

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 1135	. 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  1144  f1dom3fv3dif  7287  f1dom3el3dif  7288  f1prex  7303  oeeui  8638  oeeu  8639  domssex2  9175  domssex  9176  cantnflem1a  9722  cantnflem1b  9723  cantnflem1c  9724  cantnflem1d  9725  cantnflem1  9726  cantnflem3  9728  cantnflem4  9729  fpwwe2lem6  10673  canthnumlem  10685  canthp1lem2  10690  wuntr  10742  lelttrdi  11420  supmul1  12234  supmullem1  12235  supmullem2  12236  supmul  12237  ixxdisj  13398  ixxun  13399  ixxss1  13401  ixxss2  13402  ixxss12  13403  ixxub  13404  ixxlb  13405  iccss2  13454  iocssre  13463  icossre  13464  iccssre  13465  icodisj  13512  iccf1o  13532  xov1plusxeqvd  13534  fzen  13577  intfracq  13895  fldiv  13896  remul  15164  01sqrexlem6  15282  resqrtth  15290  sqrtth  15399  ruclem6  16267  ruclem9  16270  ruclem12  16273  gcdn0cl  16535  crth  16811  phimullem  16812  eulerthlem1  16814  eulerthlem2  16815  pcpremul  16876  prmreclem3  16951  sectcan  17802  sectco  17803  sectmon  17829  monsect  17830  funcf1  17916  funcsect  17922  invfuc  18030  coapm  18124  catciso  18164  psrel  18626  pstr  18634  mhmf  18814  submss  18834  eqger  19208  eqgcpbl  19212  gaorber  19338  orbstafun  19341  cayleyth  19447  dprdgrp  20039  dprdff  20046  ablfac1a  20103  ablfac1b  20104  lmodvscl  20892  lbsss  21093  2idlcpblrng  21298  mpfind  22148  mdetunilem2  22634  mdetunilem5  22637  mdetunilem6  22638  chfacfisfcpmat  22876  cnptop1  23265  lmfpm  23318  lmff  23324  lmcnp  23327  flimtop  23988  tlmtmd  24210  ustssxp  24228  ustdiag  24232  ustfilxp  24236  ustbas2  24249  tusbas  24292  imasdsf1olem  24398  xmeter  24458  tmsbas  24511  metustexhalf  24584  nlmngp  24713  qdensere  24805  blcvx  24833  tgqioo  24835  icccmplem2  24858  reconnlem1  24861  cnmpopc  24968  icoopnst  24982  iocopnst  24983  iccpnfcnv  24988  phtpcer  25040  phtpcco2  25045  pcohtpylem  25065  pcohtpy  25066  pcopt  25068  pcopt2  25069  pcorevlem  25072  pcorev2  25074  pcophtb  25075  om1addcl  25079  pi1grplem  25095  pi1inv  25098  pi1xfrf  25099  pi1xfr  25101  pi1xfrcnvlem  25102  pi1xfrcnv  25103  pi1cof  25105  pi1coghm  25107  cphphl  25218  cphreccllem  25225  cphsqrtcl2  25233  phclm  25279  tcphcph  25284  lmcau  25360  bcthlem4  25374  minveclem4c  25472  minveclem2  25473  minveclem3b  25475  minveclem4  25479  minveclem6  25481  ivthicc  25506  ovolfsval  25518  ovollb2lem  25536  ovolshftlem1  25557  ovolscalem1  25561  ovolicc2lem2  25566  ovolicc2lem5  25569  ovolicopnf  25572  ioombl1lem1  25606  ioombl1lem3  25608  ioombl1lem4  25609  uniioovol  25627  uniioombllem2a  25630  uniioombllem2  25631  uniioombllem3a  25632  uniioombllem3  25633  uniioombllem4  25634  uniioombllem6  25636  vitalilem2  25657  vitalilem3  25658  vitalilem4  25659  i1ff  25724  itg2monolem1  25799  itgreval  25846  ibladd  25870  iblabslem  25877  itgspliticc  25886  itgsplitioo  25887  ditgcl  25907  ditgswap  25908  ditgsplitlem  25909  ditgsplit  25910  limcresi  25934  dvlip2  26048  dveq0  26053  dvcnvre  26072  dvfsumlem2  26081  dvfsumlem2OLD  26082  ftc1a  26092  ply1rem  26219  facth1  26220  fta1glem1  26221  fta1glem2  26222  ig1pcl  26232  ig1pdvds  26233  plyrem  26361  facth  26362  vieta1lem1  26366  vieta1lem2  26367  aaliou3lem3  26400  aaliou3lem7  26405  pserulm  26479  psercnlem2  26482  psercn  26484  pserdvlem1  26485  pserdvlem2  26486  pserdv  26487  abelth2  26500  coseq00topi  26558  coseq0negpitopi  26559  cosordlem  26586  efif1olem1  26598  dvloglem  26704  loglesqrt  26818  relogbval  26829  nnlogbexp  26838  logbrec  26839  quart1  26913  quartlem2  26915  quartlem3  26916  quartlem4  26917  quart  26918  asinsinlem  26948  atanlogsublem  26972  atans2  26988  dvatan  26992  rlimcnp2  27023  divsqrtsumlem  27037  ftalem5  27134  ftalem7  27136  basellem4  27141  basellem5  27142  perfectlem2  27288  dchrinv  27319  chpdifbndlem1  27611  pntibndlem2  27649  pntlema  27654  pntlemb  27655  pntlemg  27656  pntlemh  27657  pntlemn  27658  pntlemq  27659  pntlemr  27660  pntlemj  27661  pntlemf  27663  pntlemk  27664  pntlemo  27665  pntlemp  27668  pntleml  27669  abvcxp  27673  scutcl  27861  scutun12  27869  sltrec  27879  addsproplem6  28021  addsprop  28023  addscld  28027  negsproplem6  28079  negsprop  28081  mulsproplem11  28166  mulsproplem12  28167  axtgbtwnid  28488  cgr3simp1  28542  hlne1  28627  hltr  28632  btwnhl  28636  mirhl  28701  opphllem4  28772  hlpasch  28778  inagswap  28863  inagne1  28864  dfcgrg2  28885  wlkf  29646  wlk1ewlk  29672  2wlkdlem6  29960  2wlkond  29966  2trlond  29968  grpofo  30527  vcablo  30597  nvvc  30643  sspba  30755  sspg  30756  minvecolem2  30903  minvecolem4c  30907  minvecolem4  30908  minvecolem5  30909  minvecolem6  30910  eleigveccl  31987  xrofsup  32777  eliccelico  32785  elicoelioo  32786  cyc3evpm  33152  slmdvscl  33202  slmdvsass  33205  imaslmod  33360  prmidlidl  33451  mxidlidl  33470  0ringmon1p  33562  irngss  33701  algextdeglem1  33722  baselsiga  34095  insiga  34117  ldsysgenld  34140  sigapildsys  34142  ldgenpisyslem1  34143  measfrge0  34183  sibfmbl  34316  eulerpartlemt  34352  eulerpartlemmf  34356  probfinmeasbALTV  34410  tg5segofs  34666  pfxwlk  35107  revwlk  35108  subgrwlk  35116  subfacp1lem2a  35164  subfacp1lem2b  35165  subfacp1lem3  35166  subfacp1lem4  35167  subfacp1lem5  35168  sconnpht2  35222  sconnpi1  35223  cvxsconn  35227  cvmlift2lem3  35289  cvmlift2lem5  35291  cvmlift2lem6  35292  cvmlift2lem7  35293  cvmlift2lem12  35298  cvmliftphtlem  35301  cvmliftpht  35302  cvmlift3lem2  35304  cvmlift3lem4  35306  cvmlift3lem5  35307  cvmlift3lem6  35308  msrf  35526  elmsta  35532  mthmpps  35566  mclsppslem  35567  mclspps  35568  weiunfrlem  36446  weiunpo  36447  weiunso  36448  weiunfr  36449  weiunse  36450  iblabsnclem  37669  dvasin  37690  isbnd3  37770  heiborlem3  37799  iccbnd  37826  rngohomf  37952  idlss  38002  lshplss  38962  opoccl  39175  opococ  39176  oplecon3  39180  hloml  39338  lclkrslem1  41519  lclkrslem2  41520  dvrelog2  42045  dvrelog3  42046  aks4d1p1p5  42056  primrootsunit1  42078  primrootscoprmpow  42080  primrootscoprbij  42083  primrootspoweq0  42087  aks6d1c1p2  42090  aks6d1c1p3  42091  aks6d1c1p4  42092  aks6d1c1p5  42093  aks6d1c1p7  42094  aks6d1c1p6  42095  aks6d1c1p8  42096  aks6d1c2lem3  42107  aks6d1c2lem4  42108  aks6d1c2  42111  aks6d1c6lem2  42152  aks6d1c6lem3  42153  aks6d1c6lem4  42154  aks6d1c6isolem1  42155  aks6d1c6isolem2  42156  aks6d1c6lem5  42158  aks5lem1  42167  aks5lem2  42168  aks5lem3a  42170  metakunt8  42193  metakunt19  42204  metakunt21  42206  metakunt22  42207  metakunt25  42210  evlsval3  42545  flt4lem5f  42643  flt4lem7  42645  nna4b4nsq  42646  eliccre  45457  eliocre  45461  icoiccdif  45476  limccog  45575  lptioo1  45587  cncfiooicclem1  45848  ditgeqiooicc  45915  stoweidlem30  45985  stoweidlem31  45986  stoweidlem38  45993  stoweidlem44  45999  fourierdlem26  46088  fourierdlem32  46094  fourierdlem33  46095  fourierdlem37  46099  fourierdlem42  46104  fourierdlem54  46115  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem69  46130  fourierdlem79  46140  fourierdlem82  46143  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem111  46172  0sal  46275  hoidmv1lelem3  46548  smfdmss  46688  sigardiv  46816  sigarcol  46819  sharhght  46820  sigaradd  46821  cevathlem1  46822  cevathlem2  46823  cevath  46824  proththd  47538  perfectALTVlem2  47646  isuspgrim0  47809  gpgnbgrvtx0  47964  gpgnbgrvtx1  47965  itsclc0yqsol  48613