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 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  simp1bi  1146  f1dom3fv3dif  7267  f1dom3el3dif  7268  f1prex  7282  oeeui  8602  oeeu  8603  domssex2  9137  domssex  9138  cantnflem1a  9680  cantnflem1b  9681  cantnflem1c  9682  cantnflem1d  9683  cantnflem1  9684  cantnflem3  9686  cantnflem4  9687  fpwwe2lem6  10631  canthnumlem  10643  canthp1lem2  10648  wuntr  10700  lelttrdi  11376  supmul1  12183  supmullem1  12184  supmullem2  12185  supmul  12186  ixxdisj  13339  ixxun  13340  ixxss1  13342  ixxss2  13343  ixxss12  13344  ixxub  13345  ixxlb  13346  iccss2  13395  iocssre  13404  icossre  13405  iccssre  13406  icodisj  13453  iccf1o  13473  xov1plusxeqvd  13475  fzen  13518  intfracq  13824  fldiv  13825  remul  15076  01sqrexlem6  15194  resqrtth  15202  sqrtth  15311  ruclem6  16178  ruclem9  16181  ruclem12  16184  gcdn0cl  16443  crth  16711  phimullem  16712  eulerthlem1  16714  eulerthlem2  16715  pcpremul  16776  prmreclem3  16851  sectcan  17702  sectco  17703  sectmon  17729  monsect  17730  funcf1  17816  funcsect  17822  invfuc  17927  coapm  18021  catciso  18061  psrel  18522  pstr  18530  mhmf  18677  submss  18690  eqger  19058  eqgcpbl  19062  gaorber  19172  orbstafun  19175  cayleyth  19283  dprdgrp  19875  dprdff  19882  ablfac1a  19939  ablfac1b  19940  lmodvscl  20489  lbsss  20688  2idlcpbl  20871  mpfind  21670  mdetunilem2  22115  mdetunilem5  22118  mdetunilem6  22119  chfacfisfcpmat  22357  cnptop1  22746  lmfpm  22799  lmff  22805  lmcnp  22808  flimtop  23469  tlmtmd  23691  ustssxp  23709  ustdiag  23713  ustfilxp  23717  ustbas2  23730  tusbas  23773  imasdsf1olem  23879  xmeter  23939  tmsbas  23992  metustexhalf  24065  nlmngp  24194  qdensere  24286  blcvx  24314  tgqioo  24316  icccmplem2  24339  reconnlem1  24342  cnmpopc  24444  icoopnst  24455  iocopnst  24456  iccpnfcnv  24460  phtpcer  24511  phtpcco2  24515  pcohtpylem  24535  pcohtpy  24536  pcopt  24538  pcopt2  24539  pcorevlem  24542  pcorev2  24544  pcophtb  24545  om1addcl  24549  pi1grplem  24565  pi1inv  24568  pi1xfrf  24569  pi1xfr  24571  pi1xfrcnvlem  24572  pi1xfrcnv  24573  pi1cof  24575  pi1coghm  24577  cphphl  24688  cphreccllem  24695  cphsqrtcl2  24703  phclm  24749  tcphcph  24754  lmcau  24830  bcthlem4  24844  minveclem4c  24942  minveclem2  24943  minveclem3b  24945  minveclem4  24949  minveclem6  24951  ivthicc  24975  ovolfsval  24987  ovollb2lem  25005  ovolshftlem1  25026  ovolscalem1  25030  ovolicc2lem2  25035  ovolicc2lem5  25038  ovolicopnf  25041  ioombl1lem1  25075  ioombl1lem3  25077  ioombl1lem4  25078  uniioovol  25096  uniioombllem2a  25099  uniioombllem2  25100  uniioombllem3a  25101  uniioombllem3  25102  uniioombllem4  25103  uniioombllem6  25105  vitalilem2  25126  vitalilem3  25127  vitalilem4  25128  i1ff  25193  itg2monolem1  25268  itgreval  25314  ibladd  25338  iblabslem  25345  itgspliticc  25354  itgsplitioo  25355  ditgcl  25375  ditgswap  25376  ditgsplitlem  25377  ditgsplit  25378  limcresi  25402  dvlip2  25512  dveq0  25517  dvcnvre  25536  dvfsumlem2  25544  ftc1a  25554  ply1rem  25681  facth1  25682  fta1glem1  25683  fta1glem2  25684  ig1pcl  25693  ig1pdvds  25694  plyrem  25818  facth  25819  vieta1lem1  25823  vieta1lem2  25824  aaliou3lem3  25857  aaliou3lem7  25862  pserulm  25934  psercnlem2  25936  psercn  25938  pserdvlem1  25939  pserdvlem2  25940  pserdv  25941  abelth2  25954  coseq00topi  26012  coseq0negpitopi  26013  cosordlem  26039  efif1olem1  26051  dvloglem  26156  loglesqrt  26266  relogbval  26277  nnlogbexp  26286  logbrec  26287  quart1  26361  quartlem2  26363  quartlem3  26364  quartlem4  26365  quart  26366  asinsinlem  26396  atanlogsublem  26420  atans2  26436  dvatan  26440  rlimcnp2  26471  divsqrtsumlem  26484  ftalem5  26581  ftalem7  26583  basellem4  26588  basellem5  26589  perfectlem2  26733  dchrinv  26764  chpdifbndlem1  27056  pntibndlem2  27094  pntlema  27099  pntlemb  27100  pntlemg  27101  pntlemh  27102  pntlemn  27103  pntlemq  27104  pntlemr  27105  pntlemj  27106  pntlemf  27108  pntlemk  27109  pntlemo  27110  pntlemp  27113  pntleml  27114  abvcxp  27118  scutcl  27303  scutun12  27311  sltrec  27321  addsproplem6  27458  addsprop  27460  addscld  27464  negsproplem6  27507  negsprop  27509  mulsproplem11  27582  mulsproplem12  27583  axtgbtwnid  27717  cgr3simp1  27771  hlne1  27856  hltr  27861  btwnhl  27865  mirhl  27930  opphllem4  28001  hlpasch  28007  inagswap  28092  inagne1  28093  dfcgrg2  28114  wlkf  28871  wlk1ewlk  28897  2wlkdlem6  29185  2wlkond  29191  2trlond  29193  grpofo  29752  vcablo  29822  nvvc  29868  sspba  29980  sspg  29981  minvecolem2  30128  minvecolem4c  30132  minvecolem4  30133  minvecolem5  30134  minvecolem6  30135  eleigveccl  31212  xrofsup  31980  eliccelico  31988  elicoelioo  31989  cyc3evpm  32309  slmdvscl  32359  slmdvsass  32362  imaslmod  32468  prmidlidl  32562  mxidlidl  32579  0ringmon1p  32636  irngss  32751  baselsiga  33113  insiga  33135  ldsysgenld  33158  sigapildsys  33160  ldgenpisyslem1  33161  measfrge0  33201  sibfmbl  33334  eulerpartlemt  33370  eulerpartlemmf  33374  probfinmeasbALTV  33428  tg5segofs  33685  pfxwlk  34114  revwlk  34115  subgrwlk  34123  subfacp1lem2a  34171  subfacp1lem2b  34172  subfacp1lem3  34173  subfacp1lem4  34174  subfacp1lem5  34175  sconnpht2  34229  sconnpi1  34230  cvxsconn  34234  cvmlift2lem3  34296  cvmlift2lem5  34298  cvmlift2lem6  34299  cvmlift2lem7  34300  cvmlift2lem12  34305  cvmliftphtlem  34308  cvmliftpht  34309  cvmlift3lem2  34311  cvmlift3lem4  34313  cvmlift3lem5  34314  cvmlift3lem6  34315  msrf  34533  elmsta  34539  mthmpps  34573  mclsppslem  34574  mclspps  34575  gg-dvfsumlem2  35183  iblabsnclem  36551  dvasin  36572  isbnd3  36652  heiborlem3  36681  iccbnd  36708  rngohomf  36834  idlss  36884  lshplss  37851  opoccl  38064  opococ  38065  oplecon3  38069  hloml  38227  lclkrslem1  40408  lclkrslem2  40409  dvrelog2  40929  dvrelog3  40930  aks4d1p1p5  40940  metakunt8  40992  metakunt19  41003  metakunt21  41005  metakunt22  41006  metakunt25  41009  evlsval3  41131  flt4lem5f  41399  flt4lem7  41401  nna4b4nsq  41402  eliccre  44218  eliocre  44222  icoiccdif  44237  limccog  44336  lptioo1  44348  cncfiooicclem1  44609  ditgeqiooicc  44676  stoweidlem30  44746  stoweidlem31  44747  stoweidlem38  44754  stoweidlem44  44760  fourierdlem26  44849  fourierdlem32  44855  fourierdlem33  44856  fourierdlem37  44860  fourierdlem42  44865  fourierdlem54  44876  fourierdlem63  44885  fourierdlem64  44886  fourierdlem65  44887  fourierdlem69  44891  fourierdlem79  44901  fourierdlem82  44904  fourierdlem89  44911  fourierdlem90  44912  fourierdlem91  44913  fourierdlem111  44933  0sal  45036  hoidmv1lelem3  45309  smfdmss  45449  sigardiv  45577  sigarcol  45580  sharhght  45581  sigaradd  45582  cevathlem1  45583  cevathlem2  45584  cevath  45585  proththd  46282  perfectALTVlem2  46390  2idlcpblrng  46766  itsclc0yqsol  47450