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  7298  f1dom3el3dif  7299  f1prex  7318  oeeui  8642  oeeu  8643  domssex2  9187  domssex  9188  cantnflem1a  9716  cantnflem1b  9717  cantnflem1c  9718  cantnflem1d  9719  cantnflem1  9720  cantnflem3  9722  cantnflem4  9723  fpwwe2lem6  10751  canthnumlem  10763  canthp1lem2  10768  wuntr  10820  lelttrdi  11502  supmul1  12316  supmullem1  12317  supmullem2  12318  supmul  12319  ixxdisj  13521  ixxun  13522  ixxss1  13524  ixxss2  13525  ixxss12  13526  ixxub  13527  ixxlb  13528  iccss2  13578  iocssre  13588  icossre  13589  iccssre  13590  icodisj  13637  iccf1o  13657  xov1plusxeqvd  13659  fzen  13704  intfracq  14029  fldiv  14030  remul  15328  01sqrexlem6  15446  resqrtth  15454  sqrtth  15564  ruclem6  16435  ruclem9  16438  ruclem12  16441  gcdn0cl  16704  crth  16987  phimullem  16988  eulerthlem1  16990  eulerthlem2  16991  pcpremul  17053  prmreclem3  17128  sectcan  17962  sectco  17963  sectmon  17989  monsect  17990  funcf1  18073  funcsect  18079  invfuc  18184  coapm  18278  catciso  18318  psrel  18775  pstr  18783  mhmf  19016  submss  19036  eqger  19422  eqgcpbl  19426  gaorber  19555  orbstafun  19558  cayleyth  19662  dprdgrp  20254  dprdff  20261  ablfac1a  20318  ablfac1b  20319  lmodvscl  21186  lbsss  21385  2idlcpblrng  21598  prmidlidl  21658  evlsval3  22431  mpfind  22457  mdetunilem2  22961  mdetunilem5  22964  mdetunilem6  22965  chfacfisfcpmat  23206  cnptop1  23593  lmfpm  23646  lmff  23652  lmcnp  23655  flimtop  24317  tlmtmd  24539  ustssxp  24557  ustdiag  24561  ustfilxp  24565  ustbas2  24577  tusbas  24619  imasdsf1olem  24725  xmeter  24785  tmsbas  24835  metustexhalf  24908  nlmngp  25029  qdensere  25121  blcvx  25150  tgqioo  25152  icccmplem2  25176  reconnlem1  25179  cnmpopc  25282  icoopnst  25293  iocopnst  25294  iccpnfcnv  25298  phtpcer  25349  phtpcco2  25353  pcohtpylem  25373  pcohtpy  25374  pcopt  25376  pcopt2  25377  pcorevlem  25380  pcorev2  25382  pcophtb  25383  om1addcl  25387  pi1grplem  25403  pi1inv  25406  pi1xfrf  25407  pi1xfr  25409  pi1xfrcnvlem  25410  pi1xfrcnv  25411  pi1cof  25413  pi1coghm  25415  cphphl  25525  cphreccllem  25532  cphsqrtcl2  25540  phclm  25586  tcphcph  25591  lmcau  25667  bcthlem4  25681  minveclem4c  25779  minveclem2  25780  minveclem3b  25782  minveclem4  25786  minveclem6  25788  ivthicc  25812  ovolfsval  25824  ovollb2lem  25842  ovolshftlem1  25863  ovolscalem1  25867  ovolicc2lem2  25872  ovolicc2lem5  25875  ovolicopnf  25878  ioombl1lem1  25912  ioombl1lem3  25914  ioombl1lem4  25915  uniioovol  25933  uniioombllem2a  25936  uniioombllem2  25937  uniioombllem3a  25938  uniioombllem3  25939  uniioombllem4  25940  uniioombllem6  25942  vitalilem2  25963  vitalilem3  25964  vitalilem4  25965  i1ff  26030  itg2monolem1  26104  itgreval  26150  ibladd  26174  iblabslem  26181  itgspliticc  26190  itgsplitioo  26191  ditgcl  26211  ditgswap  26212  ditgsplitlem  26213  ditgsplit  26214  limcresi  26238  dvlip2  26348  dveq0  26353  dvcnvre  26372  dvfsumlem2  26380  ftc1a  26390  ply1rem  26517  facth1  26518  fta1glem1  26519  fta1glem2  26520  ig1pcl  26530  ig1pdvds  26531  plyrem  26659  facth  26660  vieta1lem1  26666  vieta1lem2  26667  aaliou3lem3  26704  aaliou3lem7  26709  pserulm  26782  psercnlem2  26784  psercn  26786  pserdvlem1  26787  pserdvlem2  26788  pserdv  26789  abelth2  26802  coseq00topi  26864  coseq0negpitopi  26865  cosordlem  26891  efif1olem1  26903  dvloglem  27009  loglesqrt  27122  relogbval  27133  nnlogbexp  27142  logbrec  27143  quart1  27217  quartlem2  27219  quartlem3  27220  quartlem4  27221  quart  27222  asinsinlem  27252  atanlogsublem  27276  atans2  27292  dvatan  27296  rlimcnp2  27327  divsqrtsumlem  27340  ftalem5  27437  ftalem7  27439  basellem4  27444  basellem5  27445  perfectlem2  27590  dchrinv  27621  chpdifbndlem1  27913  pntibndlem2  27951  pntlema  27956  pntlemb  27957  pntlemg  27958  pntlemh  27959  pntlemn  27960  pntlemq  27961  pntlemr  27962  pntlemj  27963  pntlemf  27965  pntlemk  27966  pntlemo  27967  pntlemp  27970  pntleml  27971  abvcxp  27975  flt4lem5f  28020  flt4lem7  28022  nna4b4nsq  28023  cutscl  28201  cutsun12  28209  ltsrec  28220  addsproplem6  28393  addsprop  28395  addscld  28399  negsproplem6  28452  negsprop  28454  mulsproplem11  28545  mulsproplem12  28546  axtgbtwnid  28961  cgr3simp1  29016  hlne1  29104  hltr  29109  btwnhl  29113  mirhl  29184  opphllem4  29259  hlpasch  29267  inagswap  29393  inagne1  29394  dfcgrg2  29441  wlkf  30228  wlk1ewlk  30253  pfxwlk  30299  revwlk  30300  subgrwlk  30302  2wlkdlem6  30553  2wlkond  30559  2trlond  30561  grpofo  31134  vcablo  31204  nvvc  31250  sspba  31362  sspg  31363  minvecolem2  31510  minvecolem4c  31514  minvecolem4  31515  minvecolem5  31516  minvecolem6  31517  eleigveccl  32594  iscgrag  33085  cgrgptxfr  33086  inagcgratrgncol  33090  tgaasne  33115  tpssad  33210  xrofsup  33432  eliccelico  33442  elicoelioo  33443  cyc3evpm  33787  slmdvscl  33851  slmdvsass  33854  imaslmod  33998  mxidlidl  34072  0ringmon1p  34172  irngss  34402  algextdeglem1  34432  constrsqrtcl  34494  baselsiga  34830  insiga  34853  ldsysgenld  34876  sigapildsys  34878  ldgenpisyslem1  34879  measfrge0  34919  sibfmbl  35050  eulerpartlemt  35086  eulerpartlemmf  35090  probfinmeasbALTV  35144  tg5segofs  35388  dfk12  36025  subfacp1lem2a  36125  subfacp1lem2b  36126  subfacp1lem3  36127  subfacp1lem4  36128  subfacp1lem5  36129  sconnpht2  36183  sconnpi1  36184  cvxsconn  36188  cvmlift2lem3  36250  cvmlift2lem5  36252  cvmlift2lem6  36253  cvmlift2lem7  36254  cvmlift2lem12  36259  cvmliftphtlem  36262  cvmliftpht  36263  cvmlift3lem2  36265  cvmlift3lem4  36267  cvmlift3lem5  36268  cvmlift3lem6  36269  msrf  36487  elmsta  36493  mthmpps  36527  mclsppslem  36528  mclspps  36529  weiunfrlem  37443  weiunpo  37444  weiunso  37445  weiunfr  37446  weiunse  37447  iblabsnclem  38806  dvasin  38827  isbnd3  38921  heiborlem3  38950  iccbnd  38977  rngohomf  39103  idlss  39153  lshplss  40241  opoccl  40454  opococ  40455  oplecon3  40459  hloml  40617  lclkrslem1  42797  lclkrslem2  42798  dvrelog2  43317  dvrelog3  43318  aks4d1p1p5  43328  primrootsunit1  43350  primrootscoprmpow  43352  primrootscoprbij  43355  primrootspoweq0  43359  aks6d1c1p2  43362  aks6d1c1p3  43363  aks6d1c1p4  43364  aks6d1c1p5  43365  aks6d1c1p7  43366  aks6d1c1p6  43367  aks6d1c1p8  43368  aks6d1c2lem3  43379  aks6d1c2lem4  43380  aks6d1c2  43383  aks6d1c6lem2  43424  aks6d1c6lem3  43425  aks6d1c6lem4  43426  aks6d1c6isolem1  43427  aks6d1c6isolem2  43428  aks6d1c6lem5  43430  aks5lem1  43439  aks5lem2  43440  aks5lem3a  43442  eliccre  46732  eliocre  46736  icoiccdif  46751  limccog  46847  lptioo1  46859  cncfiooicclem1  47118  ditgeqiooicc  47185  stoweidlem30  47255  stoweidlem31  47256  stoweidlem38  47263  stoweidlem44  47269  fourierdlem26  47358  fourierdlem32  47364  fourierdlem33  47365  fourierdlem37  47369  fourierdlem42  47374  fourierdlem54  47385  fourierdlem63  47394  fourierdlem64  47395  fourierdlem65  47396  fourierdlem69  47400  fourierdlem79  47410  fourierdlem82  47413  fourierdlem89  47420  fourierdlem90  47421  fourierdlem91  47422  fourierdlem111  47442  0sal  47545  hoidmv1lelem3  47818  smfdmss  47958  sigardiv  48086  sigarcol  48089  sharhght  48090  sigaradd  48091  cevathlem1  48092  cevathlem2  48093  cevath  48094  proththd  48914  perfectALTVlem2  49035  isuspgrim0  49207  gpgnbgrvtx0  49387  gpgnbgrvtx1  49388  itsclc0yqsol  50091  imaf1hom  50439  parcatid2  50978  parcatid  50979  rr3fv1cld  51259