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  7272  f1dom3el3dif  7273  f1prex  7292  oeeui  8614  oeeu  8615  domssex2  9159  domssex  9160  cantnflem1a  9689  cantnflem1b  9690  cantnflem1c  9691  cantnflem1d  9692  cantnflem1  9693  cantnflem3  9695  cantnflem4  9696  fpwwe2lem6  10724  canthnumlem  10736  canthp1lem2  10741  wuntr  10793  lelttrdi  11475  supmul1  12289  supmullem1  12290  supmullem2  12291  supmul  12292  ixxdisj  13494  ixxun  13495  ixxss1  13497  ixxss2  13498  ixxss12  13499  ixxub  13500  ixxlb  13501  iccss2  13551  iocssre  13561  icossre  13562  iccssre  13563  icodisj  13610  iccf1o  13630  xov1plusxeqvd  13632  fzen  13677  intfracq  14002  fldiv  14003  remul  15301  01sqrexlem6  15419  resqrtth  15427  sqrtth  15537  ruclem6  16408  ruclem9  16411  ruclem12  16414  gcdn0cl  16677  crth  16960  phimullem  16961  eulerthlem1  16963  eulerthlem2  16964  pcpremul  17026  prmreclem3  17101  sectcan  17935  sectco  17936  sectmon  17962  monsect  17963  funcf1  18046  funcsect  18052  invfuc  18157  coapm  18251  catciso  18291  psrel  18748  pstr  18756  mhmf  18989  submss  19009  eqger  19395  eqgcpbl  19399  gaorber  19527  orbstafun  19530  cayleyth  19634  dprdgrp  20226  dprdff  20233  ablfac1a  20290  ablfac1b  20291  lmodvscl  21158  lbsss  21357  2idlcpblrng  21570  prmidlidl  21630  evlsval3  22403  mpfind  22429  mdetunilem2  22933  mdetunilem5  22936  mdetunilem6  22937  chfacfisfcpmat  23178  cnptop1  23565  lmfpm  23618  lmff  23624  lmcnp  23627  flimtop  24289  tlmtmd  24511  ustssxp  24529  ustdiag  24533  ustfilxp  24537  ustbas2  24549  tusbas  24591  imasdsf1olem  24697  xmeter  24757  tmsbas  24807  metustexhalf  24880  nlmngp  25001  qdensere  25093  blcvx  25122  tgqioo  25124  icccmplem2  25148  reconnlem1  25151  cnmpopc  25254  icoopnst  25265  iocopnst  25266  iccpnfcnv  25270  phtpcer  25321  phtpcco2  25325  pcohtpylem  25345  pcohtpy  25346  pcopt  25348  pcopt2  25349  pcorevlem  25352  pcorev2  25354  pcophtb  25355  om1addcl  25359  pi1grplem  25375  pi1inv  25378  pi1xfrf  25379  pi1xfr  25381  pi1xfrcnvlem  25382  pi1xfrcnv  25383  pi1cof  25385  pi1coghm  25387  cphphl  25497  cphreccllem  25504  cphsqrtcl2  25512  phclm  25558  tcphcph  25563  lmcau  25639  bcthlem4  25653  minveclem4c  25751  minveclem2  25752  minveclem3b  25754  minveclem4  25758  minveclem6  25760  ivthicc  25784  ovolfsval  25796  ovollb2lem  25814  ovolshftlem1  25835  ovolscalem1  25839  ovolicc2lem2  25844  ovolicc2lem5  25847  ovolicopnf  25850  ioombl1lem1  25884  ioombl1lem3  25886  ioombl1lem4  25887  uniioovol  25905  uniioombllem2a  25908  uniioombllem2  25909  uniioombllem3a  25910  uniioombllem3  25911  uniioombllem4  25912  uniioombllem6  25914  vitalilem2  25935  vitalilem3  25936  vitalilem4  25937  i1ff  26002  itg2monolem1  26076  itgreval  26122  ibladd  26146  iblabslem  26153  itgspliticc  26162  itgsplitioo  26163  ditgcl  26183  ditgswap  26184  ditgsplitlem  26185  ditgsplit  26186  limcresi  26210  dvlip2  26320  dveq0  26325  dvcnvre  26344  dvfsumlem2  26352  ftc1a  26362  ply1rem  26489  facth1  26490  fta1glem1  26491  fta1glem2  26492  ig1pcl  26502  ig1pdvds  26503  plyrem  26631  facth  26632  vieta1lem1  26638  vieta1lem2  26639  aaliou3lem3  26676  aaliou3lem7  26681  pserulm  26754  psercnlem2  26756  psercn  26758  pserdvlem1  26759  pserdvlem2  26760  pserdv  26761  abelth2  26774  coseq00topi  26836  coseq0negpitopi  26837  cosordlem  26863  efif1olem1  26875  dvloglem  26981  loglesqrt  27094  relogbval  27105  nnlogbexp  27114  logbrec  27115  quart1  27189  quartlem2  27191  quartlem3  27192  quartlem4  27193  quart  27194  asinsinlem  27224  atanlogsublem  27248  atans2  27264  dvatan  27268  rlimcnp2  27299  divsqrtsumlem  27312  ftalem5  27409  ftalem7  27411  basellem4  27416  basellem5  27417  perfectlem2  27562  dchrinv  27593  chpdifbndlem1  27885  pntibndlem2  27923  pntlema  27928  pntlemb  27929  pntlemg  27930  pntlemh  27931  pntlemn  27932  pntlemq  27933  pntlemr  27934  pntlemj  27935  pntlemf  27937  pntlemk  27938  pntlemo  27939  pntlemp  27942  pntleml  27943  abvcxp  27947  flt4lem5f  27992  flt4lem7  27994  nna4b4nsq  27995  cutscl  28173  cutsun12  28181  ltsrec  28192  addsproplem6  28365  addsprop  28367  addscld  28371  negsproplem6  28424  negsprop  28426  mulsproplem11  28517  mulsproplem12  28518  axtgbtwnid  28933  cgr3simp1  28988  hlne1  29076  hltr  29081  btwnhl  29085  mirhl  29156  opphllem4  29231  hlpasch  29239  inagswap  29365  inagne1  29366  dfcgrg2  29413  wlkf  30200  wlk1ewlk  30225  pfxwlk  30271  revwlk  30272  subgrwlk  30274  2wlkdlem6  30525  2wlkond  30531  2trlond  30533  grpofo  31106  vcablo  31176  nvvc  31222  sspba  31334  sspg  31335  minvecolem2  31482  minvecolem4c  31486  minvecolem4  31487  minvecolem5  31488  minvecolem6  31489  eleigveccl  32566  iscgrag  33057  cgrgptxfr  33058  inagcgratrgncol  33062  tgaasne  33087  tpssad  33182  xrofsup  33405  eliccelico  33415  elicoelioo  33416  cyc3evpm  33757  slmdvscl  33821  slmdvsass  33824  imaslmod  33960  mxidlidl  34034  0ringmon1p  34135  irngss  34365  algextdeglem1  34395  constrsqrtcl  34457  baselsiga  34793  insiga  34816  ldsysgenld  34839  sigapildsys  34841  ldgenpisyslem1  34842  measfrge0  34882  sibfmbl  35013  eulerpartlemt  35049  eulerpartlemmf  35053  probfinmeasbALTV  35107  tg5segofs  35351  subfacp1lem2a  36031  subfacp1lem2b  36032  subfacp1lem3  36033  subfacp1lem4  36034  subfacp1lem5  36035  sconnpht2  36089  sconnpi1  36090  cvxsconn  36094  cvmlift2lem3  36156  cvmlift2lem5  36158  cvmlift2lem6  36159  cvmlift2lem7  36160  cvmlift2lem12  36165  cvmliftphtlem  36168  cvmliftpht  36169  cvmlift3lem2  36171  cvmlift3lem4  36173  cvmlift3lem5  36174  cvmlift3lem6  36175  msrf  36393  elmsta  36399  mthmpps  36433  mclsppslem  36434  mclspps  36435  weiunfrlem  37344  weiunpo  37345  weiunso  37346  weiunfr  37347  weiunse  37348  iblabsnclem  38694  dvasin  38715  isbnd3  38811  heiborlem3  38840  iccbnd  38867  rngohomf  38993  idlss  39043  lshplss  40131  opoccl  40344  opococ  40345  oplecon3  40349  hloml  40507  lclkrslem1  42687  lclkrslem2  42688  dvrelog2  43207  dvrelog3  43208  aks4d1p1p5  43218  primrootsunit1  43240  primrootscoprmpow  43242  primrootscoprbij  43245  primrootspoweq0  43249  aks6d1c1p2  43252  aks6d1c1p3  43253  aks6d1c1p4  43254  aks6d1c1p5  43255  aks6d1c1p7  43256  aks6d1c1p6  43257  aks6d1c1p8  43258  aks6d1c2lem3  43269  aks6d1c2lem4  43270  aks6d1c2  43273  aks6d1c6lem2  43314  aks6d1c6lem3  43315  aks6d1c6lem4  43316  aks6d1c6isolem1  43317  aks6d1c6isolem2  43318  aks6d1c6lem5  43320  aks5lem1  43329  aks5lem2  43330  aks5lem3a  43332  eliccre  46610  eliocre  46614  icoiccdif  46629  limccog  46725  lptioo1  46737  cncfiooicclem1  46996  ditgeqiooicc  47063  stoweidlem30  47133  stoweidlem31  47134  stoweidlem38  47141  stoweidlem44  47147  fourierdlem26  47236  fourierdlem32  47242  fourierdlem33  47243  fourierdlem37  47247  fourierdlem42  47252  fourierdlem54  47263  fourierdlem63  47272  fourierdlem64  47273  fourierdlem65  47274  fourierdlem69  47278  fourierdlem79  47288  fourierdlem82  47291  fourierdlem89  47298  fourierdlem90  47299  fourierdlem91  47300  fourierdlem111  47320  0sal  47423  hoidmv1lelem3  47696  smfdmss  47836  sigardiv  47964  sigarcol  47967  sharhght  47968  sigaradd  47969  cevathlem1  47970  cevathlem2  47971  cevath  47972  proththd  48792  perfectALTVlem2  48913  isuspgrim0  49085  gpgnbgrvtx0  49265  gpgnbgrvtx1  49266  itsclc0yqsol  49969  imaf1hom  50317  parcatid2  50856  parcatid  50857  rr3fv1cld  51115