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 1087

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 1089

This theorem is referenced by:  simp1bi  1145  f1dom3fv3dif  7305  f1dom3el3dif  7306  f1prex  7320  oeeui  8658  oeeu  8659  domssex2  9203  domssex  9204  cantnflem1a  9754  cantnflem1b  9755  cantnflem1c  9756  cantnflem1d  9757  cantnflem1  9758  cantnflem3  9760  cantnflem4  9761  fpwwe2lem6  10705  canthnumlem  10717  canthp1lem2  10722  wuntr  10774  lelttrdi  11452  supmul1  12264  supmullem1  12265  supmullem2  12266  supmul  12267  ixxdisj  13422  ixxun  13423  ixxss1  13425  ixxss2  13426  ixxss12  13427  ixxub  13428  ixxlb  13429  iccss2  13478  iocssre  13487  icossre  13488  iccssre  13489  icodisj  13536  iccf1o  13556  xov1plusxeqvd  13558  fzen  13601  intfracq  13910  fldiv  13911  remul  15178  01sqrexlem6  15296  resqrtth  15304  sqrtth  15413  ruclem6  16283  ruclem9  16286  ruclem12  16289  gcdn0cl  16548  crth  16825  phimullem  16826  eulerthlem1  16828  eulerthlem2  16829  pcpremul  16890  prmreclem3  16965  sectcan  17816  sectco  17817  sectmon  17843  monsect  17844  funcf1  17930  funcsect  17936  invfuc  18044  coapm  18138  catciso  18178  psrel  18639  pstr  18647  mhmf  18824  submss  18844  eqger  19218  eqgcpbl  19222  gaorber  19348  orbstafun  19351  cayleyth  19457  dprdgrp  20049  dprdff  20056  ablfac1a  20113  ablfac1b  20114  lmodvscl  20898  lbsss  21099  2idlcpblrng  21304  mpfind  22154  mdetunilem2  22640  mdetunilem5  22643  mdetunilem6  22644  chfacfisfcpmat  22882  cnptop1  23271  lmfpm  23324  lmff  23330  lmcnp  23333  flimtop  23994  tlmtmd  24216  ustssxp  24234  ustdiag  24238  ustfilxp  24242  ustbas2  24255  tusbas  24298  imasdsf1olem  24404  xmeter  24464  tmsbas  24517  metustexhalf  24590  nlmngp  24719  qdensere  24811  blcvx  24839  tgqioo  24841  icccmplem2  24864  reconnlem1  24867  cnmpopc  24974  icoopnst  24988  iocopnst  24989  iccpnfcnv  24994  phtpcer  25046  phtpcco2  25051  pcohtpylem  25071  pcohtpy  25072  pcopt  25074  pcopt2  25075  pcorevlem  25078  pcorev2  25080  pcophtb  25081  om1addcl  25085  pi1grplem  25101  pi1inv  25104  pi1xfrf  25105  pi1xfr  25107  pi1xfrcnvlem  25108  pi1xfrcnv  25109  pi1cof  25111  pi1coghm  25113  cphphl  25224  cphreccllem  25231  cphsqrtcl2  25239  phclm  25285  tcphcph  25290  lmcau  25366  bcthlem4  25380  minveclem4c  25478  minveclem2  25479  minveclem3b  25481  minveclem4  25485  minveclem6  25487  ivthicc  25512  ovolfsval  25524  ovollb2lem  25542  ovolshftlem1  25563  ovolscalem1  25567  ovolicc2lem2  25572  ovolicc2lem5  25575  ovolicopnf  25578  ioombl1lem1  25612  ioombl1lem3  25614  ioombl1lem4  25615  uniioovol  25633  uniioombllem2a  25636  uniioombllem2  25637  uniioombllem3a  25638  uniioombllem3  25639  uniioombllem4  25640  uniioombllem6  25642  vitalilem2  25663  vitalilem3  25664  vitalilem4  25665  i1ff  25730  itg2monolem1  25805  itgreval  25852  ibladd  25876  iblabslem  25883  itgspliticc  25892  itgsplitioo  25893  ditgcl  25913  ditgswap  25914  ditgsplitlem  25915  ditgsplit  25916  limcresi  25940  dvlip2  26054  dveq0  26059  dvcnvre  26078  dvfsumlem2  26087  dvfsumlem2OLD  26088  ftc1a  26098  ply1rem  26225  facth1  26226  fta1glem1  26227  fta1glem2  26228  ig1pcl  26238  ig1pdvds  26239  plyrem  26365  facth  26366  vieta1lem1  26370  vieta1lem2  26371  aaliou3lem3  26404  aaliou3lem7  26409  pserulm  26483  psercnlem2  26486  psercn  26488  pserdvlem1  26489  pserdvlem2  26490  pserdv  26491  abelth2  26504  coseq00topi  26562  coseq0negpitopi  26563  cosordlem  26590  efif1olem1  26602  dvloglem  26708  loglesqrt  26822  relogbval  26833  nnlogbexp  26842  logbrec  26843  quart1  26917  quartlem2  26919  quartlem3  26920  quartlem4  26921  quart  26922  asinsinlem  26952  atanlogsublem  26976  atans2  26992  dvatan  26996  rlimcnp2  27027  divsqrtsumlem  27041  ftalem5  27138  ftalem7  27140  basellem4  27145  basellem5  27146  perfectlem2  27292  dchrinv  27323  chpdifbndlem1  27615  pntibndlem2  27653  pntlema  27658  pntlemb  27659  pntlemg  27660  pntlemh  27661  pntlemn  27662  pntlemq  27663  pntlemr  27664  pntlemj  27665  pntlemf  27667  pntlemk  27668  pntlemo  27669  pntlemp  27672  pntleml  27673  abvcxp  27677  scutcl  27865  scutun12  27873  sltrec  27883  addsproplem6  28025  addsprop  28027  addscld  28031  negsproplem6  28083  negsprop  28085  mulsproplem11  28170  mulsproplem12  28171  axtgbtwnid  28492  cgr3simp1  28546  hlne1  28631  hltr  28636  btwnhl  28640  mirhl  28705  opphllem4  28776  hlpasch  28782  inagswap  28867  inagne1  28868  dfcgrg2  28889  wlkf  29650  wlk1ewlk  29676  2wlkdlem6  29964  2wlkond  29970  2trlond  29972  grpofo  30531  vcablo  30601  nvvc  30647  sspba  30759  sspg  30760  minvecolem2  30907  minvecolem4c  30911  minvecolem4  30912  minvecolem5  30913  minvecolem6  30914  eleigveccl  31991  xrofsup  32774  eliccelico  32782  elicoelioo  32783  cyc3evpm  33143  slmdvscl  33193  slmdvsass  33196  imaslmod  33346  prmidlidl  33437  mxidlidl  33456  0ringmon1p  33548  irngss  33687  algextdeglem1  33708  baselsiga  34079  insiga  34101  ldsysgenld  34124  sigapildsys  34126  ldgenpisyslem1  34127  measfrge0  34167  sibfmbl  34300  eulerpartlemt  34336  eulerpartlemmf  34340  probfinmeasbALTV  34394  tg5segofs  34650  pfxwlk  35091  revwlk  35092  subgrwlk  35100  subfacp1lem2a  35148  subfacp1lem2b  35149  subfacp1lem3  35150  subfacp1lem4  35151  subfacp1lem5  35152  sconnpht2  35206  sconnpi1  35207  cvxsconn  35211  cvmlift2lem3  35273  cvmlift2lem5  35275  cvmlift2lem6  35276  cvmlift2lem7  35277  cvmlift2lem12  35282  cvmliftphtlem  35285  cvmliftpht  35286  cvmlift3lem2  35288  cvmlift3lem4  35290  cvmlift3lem5  35291  cvmlift3lem6  35292  msrf  35510  elmsta  35516  mthmpps  35550  mclsppslem  35551  mclspps  35552  weiunfrlem  36430  weiunpo  36431  weiunso  36432  weiunfr  36433  weiunse  36434  iblabsnclem  37643  dvasin  37664  isbnd3  37744  heiborlem3  37773  iccbnd  37800  rngohomf  37926  idlss  37976  lshplss  38937  opoccl  39150  opococ  39151  oplecon3  39155  hloml  39313  lclkrslem1  41494  lclkrslem2  41495  dvrelog2  42021  dvrelog3  42022  aks4d1p1p5  42032  primrootsunit1  42054  primrootscoprmpow  42056  primrootscoprbij  42059  primrootspoweq0  42063  aks6d1c1p2  42066  aks6d1c1p3  42067  aks6d1c1p4  42068  aks6d1c1p5  42069  aks6d1c1p7  42070  aks6d1c1p6  42071  aks6d1c1p8  42072  aks6d1c2lem3  42083  aks6d1c2lem4  42084  aks6d1c2  42087  aks6d1c6lem2  42128  aks6d1c6lem3  42129  aks6d1c6lem4  42130  aks6d1c6isolem1  42131  aks6d1c6isolem2  42132  aks6d1c6lem5  42134  aks5lem1  42143  aks5lem2  42144  aks5lem3a  42146  metakunt8  42169  metakunt19  42180  metakunt21  42182  metakunt22  42183  metakunt25  42186  evlsval3  42514  flt4lem5f  42612  flt4lem7  42614  nna4b4nsq  42615  eliccre  45423  eliocre  45427  icoiccdif  45442  limccog  45541  lptioo1  45553  cncfiooicclem1  45814  ditgeqiooicc  45881  stoweidlem30  45951  stoweidlem31  45952  stoweidlem38  45959  stoweidlem44  45965  fourierdlem26  46054  fourierdlem32  46060  fourierdlem33  46061  fourierdlem37  46065  fourierdlem42  46070  fourierdlem54  46081  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem69  46096  fourierdlem79  46106  fourierdlem82  46109  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem111  46138  0sal  46241  hoidmv1lelem3  46514  smfdmss  46654  sigardiv  46782  sigarcol  46785  sharhght  46786  sigaradd  46787  cevathlem1  46788  cevathlem2  46789  cevath  46790  proththd  47488  perfectALTVlem2  47596  isuspgrim0  47756  itsclc0yqsol  48498