Theorem simp1d 1160

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp1bi  1163  f1dom3fv3dif  7269  f1dom3el3dif  7270  f1prex  7289  oeeui  8594  oeeu  8595  domssex2  9139  domssex  9140  cantnflem1a  9668  cantnflem1b  9669  cantnflem1c  9670  cantnflem1d  9671  cantnflem1  9672  cantnflem3  9674  cantnflem4  9675  fpwwe2lem6  10649  canthnumlem  10661  canthp1lem2  10666  wuntr  10718  lelttrdi  11400  supmul1  12212  supmullem1  12213  supmullem2  12214  supmul  12215  ixxdisj  13417  ixxun  13418  ixxss1  13420  ixxss2  13421  ixxss12  13422  ixxub  13423  ixxlb  13424  iccss2  13474  iocssre  13484  icossre  13485  iccssre  13486  icodisj  13533  iccf1o  13553  xov1plusxeqvd  13555  fzen  13599  intfracq  13924  fldiv  13925  remul  15220  01sqrexlem6  15338  resqrtth  15346  sqrtth  15456  ruclem6  16329  ruclem9  16332  ruclem12  16335  gcdn0cl  16598  crth  16875  phimullem  16876  eulerthlem1  16878  eulerthlem2  16879  pcpremul  16941  prmreclem3  17016  sectcan  17850  sectco  17851  sectmon  17877  monsect  17878  funcf1  17961  funcsect  17967  invfuc  18072  coapm  18166  catciso  18206  psrel  18663  pstr  18671  mhmf  18903  submss  18923  eqger  19309  eqgcpbl  19313  gaorber  19441  orbstafun  19444  cayleyth  19548  dprdgrp  20140  dprdff  20147  ablfac1a  20204  ablfac1b  20205  lmodvscl  21068  lbsss  21267  2idlcpblrng  21479  prmidlidl  21538  evlsval3  22311  mpfind  22337  mdetunilem2  22841  mdetunilem5  22844  mdetunilem6  22845  chfacfisfcpmat  23086  cnptop1  23473  lmfpm  23526  lmff  23532  lmcnp  23535  flimtop  24197  tlmtmd  24419  ustssxp  24437  ustdiag  24441  ustfilxp  24445  ustbas2  24457  tusbas  24499  imasdsf1olem  24605  xmeter  24665  tmsbas  24715  metustexhalf  24788  nlmngp  24909  qdensere  25001  blcvx  25030  tgqioo  25032  icccmplem2  25056  reconnlem1  25059  cnmpopc  25162  icoopnst  25173  iocopnst  25174  iccpnfcnv  25178  phtpcer  25229  phtpcco2  25233  pcohtpylem  25253  pcohtpy  25254  pcopt  25256  pcopt2  25257  pcorevlem  25260  pcorev2  25262  pcophtb  25263  om1addcl  25267  pi1grplem  25283  pi1inv  25286  pi1xfrf  25287  pi1xfr  25289  pi1xfrcnvlem  25290  pi1xfrcnv  25291  pi1cof  25293  pi1coghm  25295  cphphl  25405  cphreccllem  25412  cphsqrtcl2  25420  phclm  25466  tcphcph  25471  lmcau  25547  bcthlem4  25561  minveclem4c  25659  minveclem2  25660  minveclem3b  25662  minveclem4  25666  minveclem6  25668  ivthicc  25692  ovolfsval  25704  ovollb2lem  25722  ovolshftlem1  25743  ovolscalem1  25747  ovolicc2lem2  25752  ovolicc2lem5  25755  ovolicopnf  25758  ioombl1lem1  25792  ioombl1lem3  25794  ioombl1lem4  25795  uniioovol  25813  uniioombllem2a  25816  uniioombllem2  25817  uniioombllem3a  25818  uniioombllem3  25819  uniioombllem4  25820  uniioombllem6  25822  vitalilem2  25843  vitalilem3  25844  vitalilem4  25845  i1ff  25910  itg2monolem1  25984  itgreval  26031  ibladd  26055  iblabslem  26062  itgspliticc  26071  itgsplitioo  26072  ditgcl  26092  ditgswap  26093  ditgsplitlem  26094  ditgsplit  26095  limcresi  26119  dvlip2  26229  dveq0  26234  dvcnvre  26253  dvfsumlem2  26261  ftc1a  26271  ply1rem  26398  facth1  26399  fta1glem1  26400  fta1glem2  26401  ig1pcl  26411  ig1pdvds  26412  plyrem  26542  facth  26543  vieta1lem1  26549  vieta1lem2  26550  aaliou3lem3  26587  aaliou3lem7  26592  pserulm  26665  psercnlem2  26667  psercn  26669  pserdvlem1  26670  pserdvlem2  26671  pserdv  26672  abelth2  26685  coseq00topi  26747  coseq0negpitopi  26748  cosordlem  26775  efif1olem1  26787  dvloglem  26893  loglesqrt  27006  relogbval  27017  nnlogbexp  27026  logbrec  27027  quart1  27101  quartlem2  27103  quartlem3  27104  quartlem4  27105  quart  27106  asinsinlem  27136  atanlogsublem  27160  atans2  27176  dvatan  27180  rlimcnp2  27211  divsqrtsumlem  27224  ftalem5  27321  ftalem7  27323  basellem4  27328  basellem5  27329  perfectlem2  27474  dchrinv  27505  chpdifbndlem1  27797  pntibndlem2  27835  pntlema  27840  pntlemb  27841  pntlemg  27842  pntlemh  27843  pntlemn  27844  pntlemq  27845  pntlemr  27846  pntlemj  27847  pntlemf  27849  pntlemk  27850  pntlemo  27851  pntlemp  27854  pntleml  27855  abvcxp  27859  cutscl  28055  cutsun12  28063  ltsrec  28074  addsproplem6  28247  addsprop  28249  addscld  28253  negsproplem6  28306  negsprop  28308  mulsproplem11  28399  mulsproplem12  28400  axtgbtwnid  28815  cgr3simp1  28870  hlne1  28958  hltr  28963  btwnhl  28967  mirhl  29038  opphllem4  29113  hlpasch  29121  inagswap  29247  inagne1  29248  dfcgrg2  29295  wlkf  30082  wlk1ewlk  30107  pfxwlk  30153  revwlk  30154  subgrwlk  30156  2wlkdlem6  30407  2wlkond  30413  2trlond  30415  grpofo  30988  vcablo  31058  nvvc  31104  sspba  31216  sspg  31217  minvecolem2  31364  minvecolem4c  31368  minvecolem4  31369  minvecolem5  31370  minvecolem6  31371  eleigveccl  32448  tpssad  33022  xrofsup  33246  eliccelico  33256  elicoelioo  33257  cyc3evpm  33598  slmdvscl  33662  slmdvsass  33665  imaslmod  33801  mxidlidl  33874  0ringmon1p  33975  irngss  34205  algextdeglem1  34235  constrsqrtcl  34297  baselsiga  34633  insiga  34656  ldsysgenld  34679  sigapildsys  34681  ldgenpisyslem1  34682  measfrge0  34722  sibfmbl  34854  eulerpartlemt  34890  eulerpartlemmf  34894  probfinmeasbALTV  34948  tg5segofs  35192  subfacp1lem2a  35767  subfacp1lem2b  35768  subfacp1lem3  35769  subfacp1lem4  35770  subfacp1lem5  35771  sconnpht2  35825  sconnpi1  35826  cvxsconn  35830  cvmlift2lem3  35892  cvmlift2lem5  35894  cvmlift2lem6  35895  cvmlift2lem7  35896  cvmlift2lem12  35901  cvmliftphtlem  35904  cvmliftpht  35905  cvmlift3lem2  35907  cvmlift3lem4  35909  cvmlift3lem5  35910  cvmlift3lem6  35911  msrf  36129  elmsta  36135  mthmpps  36169  mclsppslem  36170  mclspps  36171  weiunfrlem  37091  weiunpo  37092  weiunso  37093  weiunfr  37094  weiunse  37095  iblabsnclem  38440  dvasin  38461  isbnd3  38542  heiborlem3  38571  iccbnd  38598  rngohomf  38724  idlss  38774  lshplss  39862  opoccl  40075  opococ  40076  oplecon3  40080  hloml  40238  lclkrslem1  42418  lclkrslem2  42419  dvrelog2  42938  dvrelog3  42939  aks4d1p1p5  42949  primrootsunit1  42971  primrootscoprmpow  42973  primrootscoprbij  42976  primrootspoweq0  42980  aks6d1c1p2  42983  aks6d1c1p3  42984  aks6d1c1p4  42985  aks6d1c1p5  42986  aks6d1c1p7  42987  aks6d1c1p6  42988  aks6d1c1p8  42989  aks6d1c2lem3  43000  aks6d1c2lem4  43001  aks6d1c2  43004  aks6d1c6lem2  43045  aks6d1c6lem3  43046  aks6d1c6lem4  43047  aks6d1c6isolem1  43048  aks6d1c6isolem2  43049  aks6d1c6lem5  43051  aks5lem1  43060  aks5lem2  43061  aks5lem3a  43063  flt4lem5f  43511  flt4lem7  43513  nna4b4nsq  43514  eliccre  46343  eliocre  46347  icoiccdif  46362  limccog  46458  lptioo1  46470  cncfiooicclem1  46729  ditgeqiooicc  46796  stoweidlem30  46866  stoweidlem31  46867  stoweidlem38  46874  stoweidlem44  46880  fourierdlem26  46969  fourierdlem32  46975  fourierdlem33  46976  fourierdlem37  46980  fourierdlem42  46985  fourierdlem54  46996  fourierdlem63  47005  fourierdlem64  47006  fourierdlem65  47007  fourierdlem69  47011  fourierdlem79  47021  fourierdlem82  47024  fourierdlem89  47031  fourierdlem90  47032  fourierdlem91  47033  fourierdlem111  47053  0sal  47156  hoidmv1lelem3  47429  smfdmss  47569  sigardiv  47697  sigarcol  47700  sharhght  47701  sigaradd  47702  cevathlem1  47703  cevathlem2  47704  cevath  47705  proththd  48525  perfectALTVlem2  48646  isuspgrim0  48818  gpgnbgrvtx0  48998  gpgnbgrvtx1  48999  itsclc0yqsol  49702  imaf1hom  50042  rr3fv1cld  50788