Theorem simp1d 1142

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp1bi  1145  f1dom3fv3dif  7209  f1dom3el3dif  7210  f1prex  7225  oeeui  8527  oeeu  8528  domssex2  9061  domssex  9062  cantnflem1a  9600  cantnflem1b  9601  cantnflem1c  9602  cantnflem1d  9603  cantnflem1  9604  cantnflem3  9606  cantnflem4  9607  fpwwe2lem6  10549  canthnumlem  10561  canthp1lem2  10566  wuntr  10618  lelttrdi  11296  supmul1  12112  supmullem1  12113  supmullem2  12114  supmul  12115  ixxdisj  13281  ixxun  13282  ixxss1  13284  ixxss2  13285  ixxss12  13286  ixxub  13287  ixxlb  13288  iccss2  13338  iocssre  13348  icossre  13349  iccssre  13350  icodisj  13397  iccf1o  13417  xov1plusxeqvd  13419  fzen  13462  intfracq  13781  fldiv  13782  remul  15054  01sqrexlem6  15172  resqrtth  15180  sqrtth  15290  ruclem6  16162  ruclem9  16165  ruclem12  16168  gcdn0cl  16431  crth  16707  phimullem  16708  eulerthlem1  16710  eulerthlem2  16711  pcpremul  16773  prmreclem3  16848  sectcan  17680  sectco  17681  sectmon  17707  monsect  17708  funcf1  17791  funcsect  17797  invfuc  17902  coapm  17996  catciso  18036  psrel  18493  pstr  18501  mhmf  18681  submss  18701  eqger  19075  eqgcpbl  19079  gaorber  19205  orbstafun  19208  cayleyth  19312  dprdgrp  19904  dprdff  19911  ablfac1a  19968  ablfac1b  19969  lmodvscl  20799  lbsss  20999  2idlcpblrng  21196  mpfind  22030  mdetunilem2  22516  mdetunilem5  22519  mdetunilem6  22520  chfacfisfcpmat  22758  cnptop1  23145  lmfpm  23198  lmff  23204  lmcnp  23207  flimtop  23868  tlmtmd  24090  ustssxp  24108  ustdiag  24112  ustfilxp  24116  ustbas2  24129  tusbas  24171  imasdsf1olem  24277  xmeter  24337  tmsbas  24387  metustexhalf  24460  nlmngp  24581  qdensere  24673  blcvx  24702  tgqioo  24704  icccmplem2  24728  reconnlem1  24731  cnmpopc  24838  icoopnst  24852  iocopnst  24853  iccpnfcnv  24858  phtpcer  24910  phtpcco2  24915  pcohtpylem  24935  pcohtpy  24936  pcopt  24938  pcopt2  24939  pcorevlem  24942  pcorev2  24944  pcophtb  24945  om1addcl  24949  pi1grplem  24965  pi1inv  24968  pi1xfrf  24969  pi1xfr  24971  pi1xfrcnvlem  24972  pi1xfrcnv  24973  pi1cof  24975  pi1coghm  24977  cphphl  25087  cphreccllem  25094  cphsqrtcl2  25102  phclm  25148  tcphcph  25153  lmcau  25229  bcthlem4  25243  minveclem4c  25341  minveclem2  25342  minveclem3b  25344  minveclem4  25348  minveclem6  25350  ivthicc  25375  ovolfsval  25387  ovollb2lem  25405  ovolshftlem1  25426  ovolscalem1  25430  ovolicc2lem2  25435  ovolicc2lem5  25438  ovolicopnf  25441  ioombl1lem1  25475  ioombl1lem3  25477  ioombl1lem4  25478  uniioovol  25496  uniioombllem2a  25499  uniioombllem2  25500  uniioombllem3a  25501  uniioombllem3  25502  uniioombllem4  25503  uniioombllem6  25505  vitalilem2  25526  vitalilem3  25527  vitalilem4  25528  i1ff  25593  itg2monolem1  25667  itgreval  25714  ibladd  25738  iblabslem  25745  itgspliticc  25754  itgsplitioo  25755  ditgcl  25775  ditgswap  25776  ditgsplitlem  25777  ditgsplit  25778  limcresi  25802  dvlip2  25916  dveq0  25921  dvcnvre  25940  dvfsumlem2  25949  dvfsumlem2OLD  25950  ftc1a  25960  ply1rem  26087  facth1  26088  fta1glem1  26089  fta1glem2  26090  ig1pcl  26100  ig1pdvds  26101  plyrem  26229  facth  26230  vieta1lem1  26234  vieta1lem2  26235  aaliou3lem3  26268  aaliou3lem7  26273  pserulm  26347  psercnlem2  26350  psercn  26352  pserdvlem1  26353  pserdvlem2  26354  pserdv  26355  abelth2  26368  coseq00topi  26427  coseq0negpitopi  26428  cosordlem  26455  efif1olem1  26467  dvloglem  26573  loglesqrt  26687  relogbval  26698  nnlogbexp  26707  logbrec  26708  quart1  26782  quartlem2  26784  quartlem3  26785  quartlem4  26786  quart  26787  asinsinlem  26817  atanlogsublem  26841  atans2  26857  dvatan  26861  rlimcnp2  26892  divsqrtsumlem  26906  ftalem5  27003  ftalem7  27005  basellem4  27010  basellem5  27011  perfectlem2  27157  dchrinv  27188  chpdifbndlem1  27480  pntibndlem2  27518  pntlema  27523  pntlemb  27524  pntlemg  27525  pntlemh  27526  pntlemn  27527  pntlemq  27528  pntlemr  27529  pntlemj  27530  pntlemf  27532  pntlemk  27533  pntlemo  27534  pntlemp  27537  pntleml  27538  abvcxp  27542  scutcl  27731  scutun12  27739  sltrec  27750  addsproplem6  27904  addsprop  27906  addscld  27910  negsproplem6  27962  negsprop  27964  mulsproplem11  28052  mulsproplem12  28053  axtgbtwnid  28429  cgr3simp1  28483  hlne1  28568  hltr  28573  btwnhl  28577  mirhl  28642  opphllem4  28713  hlpasch  28719  inagswap  28804  inagne1  28805  dfcgrg2  28826  wlkf  29578  wlk1ewlk  29603  2wlkdlem6  29894  2wlkond  29900  2trlond  29902  grpofo  30461  vcablo  30531  nvvc  30577  sspba  30689  sspg  30690  minvecolem2  30837  minvecolem4c  30841  minvecolem4  30842  minvecolem5  30843  minvecolem6  30844  eleigveccl  31921  tpssad  32501  xrofsup  32723  eliccelico  32733  elicoelioo  32734  cyc3evpm  33105  slmdvscl  33166  slmdvsass  33169  imaslmod  33300  prmidlidl  33391  mxidlidl  33410  0ringmon1p  33502  irngss  33658  algextdeglem1  33683  constrsqrtcl  33745  baselsiga  34081  insiga  34103  ldsysgenld  34126  sigapildsys  34128  ldgenpisyslem1  34129  measfrge0  34169  sibfmbl  34302  eulerpartlemt  34338  eulerpartlemmf  34342  probfinmeasbALTV  34396  tg5segofs  34640  pfxwlk  35096  revwlk  35097  subgrwlk  35104  subfacp1lem2a  35152  subfacp1lem2b  35153  subfacp1lem3  35154  subfacp1lem4  35155  subfacp1lem5  35156  sconnpht2  35210  sconnpi1  35211  cvxsconn  35215  cvmlift2lem3  35277  cvmlift2lem5  35279  cvmlift2lem6  35280  cvmlift2lem7  35281  cvmlift2lem12  35286  cvmliftphtlem  35289  cvmliftpht  35290  cvmlift3lem2  35292  cvmlift3lem4  35294  cvmlift3lem5  35295  cvmlift3lem6  35296  msrf  35514  elmsta  35520  mthmpps  35554  mclsppslem  35555  mclspps  35556  weiunfrlem  36437  weiunpo  36438  weiunso  36439  weiunfr  36440  weiunse  36441  iblabsnclem  37662  dvasin  37683  isbnd3  37763  heiborlem3  37792  iccbnd  37819  rngohomf  37945  idlss  37995  lshplss  38959  opoccl  39172  opococ  39173  oplecon3  39177  hloml  39335  lclkrslem1  41516  lclkrslem2  41517  dvrelog2  42037  dvrelog3  42038  aks4d1p1p5  42048  primrootsunit1  42070  primrootscoprmpow  42072  primrootscoprbij  42075  primrootspoweq0  42079  aks6d1c1p2  42082  aks6d1c1p3  42083  aks6d1c1p4  42084  aks6d1c1p5  42085  aks6d1c1p7  42086  aks6d1c1p6  42087  aks6d1c1p8  42088  aks6d1c2lem3  42099  aks6d1c2lem4  42100  aks6d1c2  42103  aks6d1c6lem2  42144  aks6d1c6lem3  42145  aks6d1c6lem4  42146  aks6d1c6isolem1  42147  aks6d1c6isolem2  42148  aks6d1c6lem5  42150  aks5lem1  42159  aks5lem2  42160  aks5lem3a  42162  evlsval3  42532  flt4lem5f  42630  flt4lem7  42632  nna4b4nsq  42633  eliccre  45487  eliocre  45491  icoiccdif  45506  limccog  45602  lptioo1  45614  cncfiooicclem1  45875  ditgeqiooicc  45942  stoweidlem30  46012  stoweidlem31  46013  stoweidlem38  46020  stoweidlem44  46026  fourierdlem26  46115  fourierdlem32  46121  fourierdlem33  46122  fourierdlem37  46126  fourierdlem42  46131  fourierdlem54  46142  fourierdlem63  46151  fourierdlem64  46152  fourierdlem65  46153  fourierdlem69  46157  fourierdlem79  46167  fourierdlem82  46170  fourierdlem89  46177  fourierdlem90  46178  fourierdlem91  46179  fourierdlem111  46199  0sal  46302  hoidmv1lelem3  46575  smfdmss  46715  sigardiv  46843  sigarcol  46846  sharhght  46847  sigaradd  46848  cevathlem1  46849  cevathlem2  46850  cevath  46851  proththd  47599  perfectALTVlem2  47707  isuspgrim0  47879  gpgnbgrvtx0  48059  gpgnbgrvtx1  48060  itsclc0yqsol  48750  imaf1hom  49094