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  7243  f1dom3el3dif  7244  f1prex  7259  oeeui  8566  oeeu  8567  domssex2  9101  domssex  9102  cantnflem1a  9638  cantnflem1b  9639  cantnflem1c  9640  cantnflem1d  9641  cantnflem1  9642  cantnflem3  9644  cantnflem4  9645  fpwwe2lem6  10589  canthnumlem  10601  canthp1lem2  10606  wuntr  10658  lelttrdi  11336  supmul1  12152  supmullem1  12153  supmullem2  12154  supmul  12155  ixxdisj  13321  ixxun  13322  ixxss1  13324  ixxss2  13325  ixxss12  13326  ixxub  13327  ixxlb  13328  iccss2  13378  iocssre  13388  icossre  13389  iccssre  13390  icodisj  13437  iccf1o  13457  xov1plusxeqvd  13459  fzen  13502  intfracq  13821  fldiv  13822  remul  15095  01sqrexlem6  15213  resqrtth  15221  sqrtth  15331  ruclem6  16203  ruclem9  16206  ruclem12  16209  gcdn0cl  16472  crth  16748  phimullem  16749  eulerthlem1  16751  eulerthlem2  16752  pcpremul  16814  prmreclem3  16889  sectcan  17717  sectco  17718  sectmon  17744  monsect  17745  funcf1  17828  funcsect  17834  invfuc  17939  coapm  18033  catciso  18073  psrel  18528  pstr  18536  mhmf  18716  submss  18736  eqger  19110  eqgcpbl  19114  gaorber  19240  orbstafun  19243  cayleyth  19345  dprdgrp  19937  dprdff  19944  ablfac1a  20001  ablfac1b  20002  lmodvscl  20784  lbsss  20984  2idlcpblrng  21181  mpfind  22014  mdetunilem2  22500  mdetunilem5  22503  mdetunilem6  22504  chfacfisfcpmat  22742  cnptop1  23129  lmfpm  23182  lmff  23188  lmcnp  23191  flimtop  23852  tlmtmd  24074  ustssxp  24092  ustdiag  24096  ustfilxp  24100  ustbas2  24113  tusbas  24155  imasdsf1olem  24261  xmeter  24321  tmsbas  24371  metustexhalf  24444  nlmngp  24565  qdensere  24657  blcvx  24686  tgqioo  24688  icccmplem2  24712  reconnlem1  24715  cnmpopc  24822  icoopnst  24836  iocopnst  24837  iccpnfcnv  24842  phtpcer  24894  phtpcco2  24899  pcohtpylem  24919  pcohtpy  24920  pcopt  24922  pcopt2  24923  pcorevlem  24926  pcorev2  24928  pcophtb  24929  om1addcl  24933  pi1grplem  24949  pi1inv  24952  pi1xfrf  24953  pi1xfr  24955  pi1xfrcnvlem  24956  pi1xfrcnv  24957  pi1cof  24959  pi1coghm  24961  cphphl  25071  cphreccllem  25078  cphsqrtcl2  25086  phclm  25132  tcphcph  25137  lmcau  25213  bcthlem4  25227  minveclem4c  25325  minveclem2  25326  minveclem3b  25328  minveclem4  25332  minveclem6  25334  ivthicc  25359  ovolfsval  25371  ovollb2lem  25389  ovolshftlem1  25410  ovolscalem1  25414  ovolicc2lem2  25419  ovolicc2lem5  25422  ovolicopnf  25425  ioombl1lem1  25459  ioombl1lem3  25461  ioombl1lem4  25462  uniioovol  25480  uniioombllem2a  25483  uniioombllem2  25484  uniioombllem3a  25485  uniioombllem3  25486  uniioombllem4  25487  uniioombllem6  25489  vitalilem2  25510  vitalilem3  25511  vitalilem4  25512  i1ff  25577  itg2monolem1  25651  itgreval  25698  ibladd  25722  iblabslem  25729  itgspliticc  25738  itgsplitioo  25739  ditgcl  25759  ditgswap  25760  ditgsplitlem  25761  ditgsplit  25762  limcresi  25786  dvlip2  25900  dveq0  25905  dvcnvre  25924  dvfsumlem2  25933  dvfsumlem2OLD  25934  ftc1a  25944  ply1rem  26071  facth1  26072  fta1glem1  26073  fta1glem2  26074  ig1pcl  26084  ig1pdvds  26085  plyrem  26213  facth  26214  vieta1lem1  26218  vieta1lem2  26219  aaliou3lem3  26252  aaliou3lem7  26257  pserulm  26331  psercnlem2  26334  psercn  26336  pserdvlem1  26337  pserdvlem2  26338  pserdv  26339  abelth2  26352  coseq00topi  26411  coseq0negpitopi  26412  cosordlem  26439  efif1olem1  26451  dvloglem  26557  loglesqrt  26671  relogbval  26682  nnlogbexp  26691  logbrec  26692  quart1  26766  quartlem2  26768  quartlem3  26769  quartlem4  26770  quart  26771  asinsinlem  26801  atanlogsublem  26825  atans2  26841  dvatan  26845  rlimcnp2  26876  divsqrtsumlem  26890  ftalem5  26987  ftalem7  26989  basellem4  26994  basellem5  26995  perfectlem2  27141  dchrinv  27172  chpdifbndlem1  27464  pntibndlem2  27502  pntlema  27507  pntlemb  27508  pntlemg  27509  pntlemh  27510  pntlemn  27511  pntlemq  27512  pntlemr  27513  pntlemj  27514  pntlemf  27516  pntlemk  27517  pntlemo  27518  pntlemp  27521  pntleml  27522  abvcxp  27526  scutcl  27714  scutun12  27722  sltrec  27732  addsproplem6  27881  addsprop  27883  addscld  27887  negsproplem6  27939  negsprop  27941  mulsproplem11  28029  mulsproplem12  28030  axtgbtwnid  28393  cgr3simp1  28447  hlne1  28532  hltr  28537  btwnhl  28541  mirhl  28606  opphllem4  28677  hlpasch  28683  inagswap  28768  inagne1  28769  dfcgrg2  28790  wlkf  29542  wlk1ewlk  29568  2wlkdlem6  29861  2wlkond  29867  2trlond  29869  grpofo  30428  vcablo  30498  nvvc  30544  sspba  30656  sspg  30657  minvecolem2  30804  minvecolem4c  30808  minvecolem4  30809  minvecolem5  30810  minvecolem6  30811  eleigveccl  31888  tpssad  32468  xrofsup  32690  eliccelico  32700  elicoelioo  32701  cyc3evpm  33107  slmdvscl  33167  slmdvsass  33170  imaslmod  33324  prmidlidl  33415  mxidlidl  33434  0ringmon1p  33526  irngss  33682  algextdeglem1  33707  constrsqrtcl  33769  baselsiga  34105  insiga  34127  ldsysgenld  34150  sigapildsys  34152  ldgenpisyslem1  34153  measfrge0  34193  sibfmbl  34326  eulerpartlemt  34362  eulerpartlemmf  34366  probfinmeasbALTV  34420  tg5segofs  34664  pfxwlk  35111  revwlk  35112  subgrwlk  35119  subfacp1lem2a  35167  subfacp1lem2b  35168  subfacp1lem3  35169  subfacp1lem4  35170  subfacp1lem5  35171  sconnpht2  35225  sconnpi1  35226  cvxsconn  35230  cvmlift2lem3  35292  cvmlift2lem5  35294  cvmlift2lem6  35295  cvmlift2lem7  35296  cvmlift2lem12  35301  cvmliftphtlem  35304  cvmliftpht  35305  cvmlift3lem2  35307  cvmlift3lem4  35309  cvmlift3lem5  35310  cvmlift3lem6  35311  msrf  35529  elmsta  35535  mthmpps  35569  mclsppslem  35570  mclspps  35571  weiunfrlem  36452  weiunpo  36453  weiunso  36454  weiunfr  36455  weiunse  36456  iblabsnclem  37677  dvasin  37698  isbnd3  37778  heiborlem3  37807  iccbnd  37834  rngohomf  37960  idlss  38010  lshplss  38974  opoccl  39187  opococ  39188  oplecon3  39192  hloml  39350  lclkrslem1  41531  lclkrslem2  41532  dvrelog2  42052  dvrelog3  42053  aks4d1p1p5  42063  primrootsunit1  42085  primrootscoprmpow  42087  primrootscoprbij  42090  primrootspoweq0  42094  aks6d1c1p2  42097  aks6d1c1p3  42098  aks6d1c1p4  42099  aks6d1c1p5  42100  aks6d1c1p7  42101  aks6d1c1p6  42102  aks6d1c1p8  42103  aks6d1c2lem3  42114  aks6d1c2lem4  42115  aks6d1c2  42118  aks6d1c6lem2  42159  aks6d1c6lem3  42160  aks6d1c6lem4  42161  aks6d1c6isolem1  42162  aks6d1c6isolem2  42163  aks6d1c6lem5  42165  aks5lem1  42174  aks5lem2  42175  aks5lem3a  42177  evlsval3  42547  flt4lem5f  42645  flt4lem7  42647  nna4b4nsq  42648  eliccre  45503  eliocre  45507  icoiccdif  45522  limccog  45618  lptioo1  45630  cncfiooicclem1  45891  ditgeqiooicc  45958  stoweidlem30  46028  stoweidlem31  46029  stoweidlem38  46036  stoweidlem44  46042  fourierdlem26  46131  fourierdlem32  46137  fourierdlem33  46138  fourierdlem37  46142  fourierdlem42  46147  fourierdlem54  46158  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem69  46173  fourierdlem79  46183  fourierdlem82  46186  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem111  46215  0sal  46318  hoidmv1lelem3  46591  smfdmss  46731  sigardiv  46859  sigarcol  46862  sharhght  46863  sigaradd  46864  cevathlem1  46865  cevathlem2  46866  cevath  46867  proththd  47615  perfectALTVlem2  47723  isuspgrim0  47894  gpgnbgrvtx0  48065  gpgnbgrvtx1  48066  itsclc0yqsol  48753  imaf1hom  49097