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  7223  f1dom3el3dif  7224  f1prex  7239  oeeui  8538  oeeu  8539  domssex2  9075  domssex  9076  cantnflem1a  9606  cantnflem1b  9607  cantnflem1c  9608  cantnflem1d  9609  cantnflem1  9610  cantnflem3  9612  cantnflem4  9613  fpwwe2lem6  10559  canthnumlem  10571  canthp1lem2  10576  wuntr  10628  lelttrdi  11308  supmul1  12125  supmullem1  12126  supmullem2  12127  supmul  12128  ixxdisj  13313  ixxun  13314  ixxss1  13316  ixxss2  13317  ixxss12  13318  ixxub  13319  ixxlb  13320  iccss2  13370  iocssre  13380  icossre  13381  iccssre  13382  icodisj  13429  iccf1o  13449  xov1plusxeqvd  13451  fzen  13495  intfracq  13818  fldiv  13819  remul  15091  01sqrexlem6  15209  resqrtth  15217  sqrtth  15327  ruclem6  16202  ruclem9  16205  ruclem12  16208  gcdn0cl  16471  crth  16748  phimullem  16749  eulerthlem1  16751  eulerthlem2  16752  pcpremul  16814  prmreclem3  16889  sectcan  17722  sectco  17723  sectmon  17749  monsect  17750  funcf1  17833  funcsect  17839  invfuc  17944  coapm  18038  catciso  18078  psrel  18535  pstr  18543  mhmf  18757  submss  18777  eqger  19153  eqgcpbl  19157  gaorber  19283  orbstafun  19286  cayleyth  19390  dprdgrp  19982  dprdff  19989  ablfac1a  20046  ablfac1b  20047  lmodvscl  20873  lbsss  21072  2idlcpblrng  21269  evlsval3  22067  mpfind  22093  mdetunilem2  22578  mdetunilem5  22581  mdetunilem6  22582  chfacfisfcpmat  22820  cnptop1  23207  lmfpm  23260  lmff  23266  lmcnp  23269  flimtop  23930  tlmtmd  24152  ustssxp  24170  ustdiag  24174  ustfilxp  24178  ustbas2  24190  tusbas  24232  imasdsf1olem  24338  xmeter  24398  tmsbas  24448  metustexhalf  24521  nlmngp  24642  qdensere  24734  blcvx  24763  tgqioo  24765  icccmplem2  24789  reconnlem1  24792  cnmpopc  24895  icoopnst  24906  iocopnst  24907  iccpnfcnv  24911  phtpcer  24962  phtpcco2  24966  pcohtpylem  24986  pcohtpy  24987  pcopt  24989  pcopt2  24990  pcorevlem  24993  pcorev2  24995  pcophtb  24996  om1addcl  25000  pi1grplem  25016  pi1inv  25019  pi1xfrf  25020  pi1xfr  25022  pi1xfrcnvlem  25023  pi1xfrcnv  25024  pi1cof  25026  pi1coghm  25028  cphphl  25138  cphreccllem  25145  cphsqrtcl2  25153  phclm  25199  tcphcph  25204  lmcau  25280  bcthlem4  25294  minveclem4c  25392  minveclem2  25393  minveclem3b  25395  minveclem4  25399  minveclem6  25401  ivthicc  25425  ovolfsval  25437  ovollb2lem  25455  ovolshftlem1  25476  ovolscalem1  25480  ovolicc2lem2  25485  ovolicc2lem5  25488  ovolicopnf  25491  ioombl1lem1  25525  ioombl1lem3  25527  ioombl1lem4  25528  uniioovol  25546  uniioombllem2a  25549  uniioombllem2  25550  uniioombllem3a  25551  uniioombllem3  25552  uniioombllem4  25553  uniioombllem6  25555  vitalilem2  25576  vitalilem3  25577  vitalilem4  25578  i1ff  25643  itg2monolem1  25717  itgreval  25764  ibladd  25788  iblabslem  25795  itgspliticc  25804  itgsplitioo  25805  ditgcl  25825  ditgswap  25826  ditgsplitlem  25827  ditgsplit  25828  limcresi  25852  dvlip2  25962  dveq0  25967  dvcnvre  25986  dvfsumlem2  25994  ftc1a  26004  ply1rem  26131  facth1  26132  fta1glem1  26133  fta1glem2  26134  ig1pcl  26144  ig1pdvds  26145  plyrem  26271  facth  26272  vieta1lem1  26276  vieta1lem2  26277  aaliou3lem3  26310  aaliou3lem7  26315  pserulm  26387  psercnlem2  26389  psercn  26391  pserdvlem1  26392  pserdvlem2  26393  pserdv  26394  abelth2  26407  coseq00topi  26466  coseq0negpitopi  26467  cosordlem  26494  efif1olem1  26506  dvloglem  26612  loglesqrt  26725  relogbval  26736  nnlogbexp  26745  logbrec  26746  quart1  26820  quartlem2  26822  quartlem3  26823  quartlem4  26824  quart  26825  asinsinlem  26855  atanlogsublem  26879  atans2  26895  dvatan  26899  rlimcnp2  26930  divsqrtsumlem  26943  ftalem5  27040  ftalem7  27042  basellem4  27047  basellem5  27048  perfectlem2  27193  dchrinv  27224  chpdifbndlem1  27516  pntibndlem2  27554  pntlema  27559  pntlemb  27560  pntlemg  27561  pntlemh  27562  pntlemn  27563  pntlemq  27564  pntlemr  27565  pntlemj  27566  pntlemf  27568  pntlemk  27569  pntlemo  27570  pntlemp  27573  pntleml  27574  abvcxp  27578  cutscl  27774  cutsun12  27782  ltsrec  27793  addsproplem6  27966  addsprop  27968  addscld  27972  negsproplem6  28025  negsprop  28027  mulsproplem11  28118  mulsproplem12  28119  axtgbtwnid  28534  cgr3simp1  28588  hlne1  28673  hltr  28678  btwnhl  28682  mirhl  28747  opphllem4  28818  hlpasch  28824  inagswap  28909  inagne1  28910  dfcgrg2  28931  wlkf  29683  wlk1ewlk  29708  2wlkdlem6  29999  2wlkond  30005  2trlond  30007  grpofo  30570  vcablo  30640  nvvc  30686  sspba  30798  sspg  30799  minvecolem2  30946  minvecolem4c  30950  minvecolem4  30951  minvecolem5  30952  minvecolem6  30953  eleigveccl  32030  tpssad  32609  xrofsup  32840  eliccelico  32850  elicoelioo  32851  cyc3evpm  33211  slmdvscl  33275  slmdvsass  33278  imaslmod  33413  prmidlidl  33504  mxidlidl  33523  0ringmon1p  33617  irngss  33831  algextdeglem1  33861  constrsqrtcl  33923  baselsiga  34259  insiga  34281  ldsysgenld  34304  sigapildsys  34306  ldgenpisyslem1  34307  measfrge0  34347  sibfmbl  34479  eulerpartlemt  34515  eulerpartlemmf  34519  probfinmeasbALTV  34573  tg5segofs  34817  pfxwlk  35306  revwlk  35307  subgrwlk  35314  subfacp1lem2a  35362  subfacp1lem2b  35363  subfacp1lem3  35364  subfacp1lem4  35365  subfacp1lem5  35366  sconnpht2  35420  sconnpi1  35421  cvxsconn  35425  cvmlift2lem3  35487  cvmlift2lem5  35489  cvmlift2lem6  35490  cvmlift2lem7  35491  cvmlift2lem12  35496  cvmliftphtlem  35499  cvmliftpht  35500  cvmlift3lem2  35502  cvmlift3lem4  35504  cvmlift3lem5  35505  cvmlift3lem6  35506  msrf  35724  elmsta  35730  mthmpps  35764  mclsppslem  35765  mclspps  35766  weiunfrlem  36646  weiunpo  36647  weiunso  36648  weiunfr  36649  weiunse  36650  iblabsnclem  38004  dvasin  38025  isbnd3  38105  heiborlem3  38134  iccbnd  38161  rngohomf  38287  idlss  38337  lshplss  39427  opoccl  39640  opococ  39641  oplecon3  39645  hloml  39803  lclkrslem1  41983  lclkrslem2  41984  dvrelog2  42503  dvrelog3  42504  aks4d1p1p5  42514  primrootsunit1  42536  primrootscoprmpow  42538  primrootscoprbij  42541  primrootspoweq0  42545  aks6d1c1p2  42548  aks6d1c1p3  42549  aks6d1c1p4  42550  aks6d1c1p5  42551  aks6d1c1p7  42552  aks6d1c1p6  42553  aks6d1c1p8  42554  aks6d1c2lem3  42565  aks6d1c2lem4  42566  aks6d1c2  42569  aks6d1c6lem2  42610  aks6d1c6lem3  42611  aks6d1c6lem4  42612  aks6d1c6isolem1  42613  aks6d1c6isolem2  42614  aks6d1c6lem5  42616  aks5lem1  42625  aks5lem2  42626  aks5lem3a  42628  flt4lem5f  43090  flt4lem7  43092  nna4b4nsq  43093  eliccre  45935  eliocre  45939  icoiccdif  45954  limccog  46050  lptioo1  46062  cncfiooicclem1  46321  ditgeqiooicc  46388  stoweidlem30  46458  stoweidlem31  46459  stoweidlem38  46466  stoweidlem44  46472  fourierdlem26  46561  fourierdlem32  46567  fourierdlem33  46568  fourierdlem37  46572  fourierdlem42  46577  fourierdlem54  46588  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem69  46603  fourierdlem79  46613  fourierdlem82  46616  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem111  46645  0sal  46748  hoidmv1lelem3  47021  smfdmss  47161  sigardiv  47289  sigarcol  47292  sharhght  47293  sigaradd  47294  cevathlem1  47295  cevathlem2  47296  cevath  47297  nthrucw  47316  proththd  48077  perfectALTVlem2  48198  isuspgrim0  48370  gpgnbgrvtx0  48550  gpgnbgrvtx1  48551  itsclc0yqsol  49240  imaf1hom  49583