Theorem simp1d 1139

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  simp1bi  1142  f1dom3fv3dif  7283  f1dom3el3dif  7284  f1prex  7298  oeeui  8632  oeeu  8633  domssex2  9175  domssex  9176  cantnflem1a  9728  cantnflem1b  9729  cantnflem1c  9730  cantnflem1d  9731  cantnflem1  9732  cantnflem3  9734  cantnflem4  9735  fpwwe2lem6  10679  canthnumlem  10691  canthp1lem2  10696  wuntr  10748  lelttrdi  11426  supmul1  12235  supmullem1  12236  supmullem2  12237  supmul  12238  ixxdisj  13393  ixxun  13394  ixxss1  13396  ixxss2  13397  ixxss12  13398  ixxub  13399  ixxlb  13400  iccss2  13449  iocssre  13458  icossre  13459  iccssre  13460  icodisj  13507  iccf1o  13527  xov1plusxeqvd  13529  fzen  13572  intfracq  13879  fldiv  13880  remul  15134  01sqrexlem6  15252  resqrtth  15260  sqrtth  15369  ruclem6  16237  ruclem9  16240  ruclem12  16243  gcdn0cl  16502  crth  16780  phimullem  16781  eulerthlem1  16783  eulerthlem2  16784  pcpremul  16845  prmreclem3  16920  sectcan  17771  sectco  17772  sectmon  17798  monsect  17799  funcf1  17885  funcsect  17891  invfuc  17999  coapm  18093  catciso  18133  psrel  18594  pstr  18602  mhmf  18779  submss  18799  eqger  19172  eqgcpbl  19176  gaorber  19302  orbstafun  19305  cayleyth  19413  dprdgrp  20005  dprdff  20012  ablfac1a  20069  ablfac1b  20070  lmodvscl  20854  lbsss  21055  2idlcpblrng  21260  mpfind  22122  mdetunilem2  22606  mdetunilem5  22609  mdetunilem6  22610  chfacfisfcpmat  22848  cnptop1  23237  lmfpm  23290  lmff  23296  lmcnp  23299  flimtop  23960  tlmtmd  24182  ustssxp  24200  ustdiag  24204  ustfilxp  24208  ustbas2  24221  tusbas  24264  imasdsf1olem  24370  xmeter  24430  tmsbas  24483  metustexhalf  24556  nlmngp  24685  qdensere  24777  blcvx  24805  tgqioo  24807  icccmplem2  24830  reconnlem1  24833  cnmpopc  24940  icoopnst  24954  iocopnst  24955  iccpnfcnv  24960  phtpcer  25012  phtpcco2  25017  pcohtpylem  25037  pcohtpy  25038  pcopt  25040  pcopt2  25041  pcorevlem  25044  pcorev2  25046  pcophtb  25047  om1addcl  25051  pi1grplem  25067  pi1inv  25070  pi1xfrf  25071  pi1xfr  25073  pi1xfrcnvlem  25074  pi1xfrcnv  25075  pi1cof  25077  pi1coghm  25079  cphphl  25190  cphreccllem  25197  cphsqrtcl2  25205  phclm  25251  tcphcph  25256  lmcau  25332  bcthlem4  25346  minveclem4c  25444  minveclem2  25445  minveclem3b  25447  minveclem4  25451  minveclem6  25453  ivthicc  25478  ovolfsval  25490  ovollb2lem  25508  ovolshftlem1  25529  ovolscalem1  25533  ovolicc2lem2  25538  ovolicc2lem5  25541  ovolicopnf  25544  ioombl1lem1  25578  ioombl1lem3  25580  ioombl1lem4  25581  uniioovol  25599  uniioombllem2a  25602  uniioombllem2  25603  uniioombllem3a  25604  uniioombllem3  25605  uniioombllem4  25606  uniioombllem6  25608  vitalilem2  25629  vitalilem3  25630  vitalilem4  25631  i1ff  25696  itg2monolem1  25771  itgreval  25817  ibladd  25841  iblabslem  25848  itgspliticc  25857  itgsplitioo  25858  ditgcl  25878  ditgswap  25879  ditgsplitlem  25880  ditgsplit  25881  limcresi  25905  dvlip2  26019  dveq0  26024  dvcnvre  26043  dvfsumlem2  26052  dvfsumlem2OLD  26053  ftc1a  26063  ply1rem  26193  facth1  26194  fta1glem1  26195  fta1glem2  26196  ig1pcl  26206  ig1pdvds  26207  plyrem  26333  facth  26334  vieta1lem1  26338  vieta1lem2  26339  aaliou3lem3  26372  aaliou3lem7  26377  pserulm  26451  psercnlem2  26454  psercn  26456  pserdvlem1  26457  pserdvlem2  26458  pserdv  26459  abelth2  26472  coseq00topi  26530  coseq0negpitopi  26531  cosordlem  26557  efif1olem1  26569  dvloglem  26675  loglesqrt  26789  relogbval  26800  nnlogbexp  26809  logbrec  26810  quart1  26884  quartlem2  26886  quartlem3  26887  quartlem4  26888  quart  26889  asinsinlem  26919  atanlogsublem  26943  atans2  26959  dvatan  26963  rlimcnp2  26994  divsqrtsumlem  27008  ftalem5  27105  ftalem7  27107  basellem4  27112  basellem5  27113  perfectlem2  27259  dchrinv  27290  chpdifbndlem1  27582  pntibndlem2  27620  pntlema  27625  pntlemb  27626  pntlemg  27627  pntlemh  27628  pntlemn  27629  pntlemq  27630  pntlemr  27631  pntlemj  27632  pntlemf  27634  pntlemk  27635  pntlemo  27636  pntlemp  27639  pntleml  27640  abvcxp  27644  scutcl  27832  scutun12  27840  sltrec  27850  addsproplem6  27988  addsprop  27990  addscld  27994  negsproplem6  28042  negsprop  28044  mulsproplem11  28127  mulsproplem12  28128  axtgbtwnid  28393  cgr3simp1  28447  hlne1  28532  hltr  28537  btwnhl  28541  mirhl  28606  opphllem4  28677  hlpasch  28683  inagswap  28768  inagne1  28769  dfcgrg2  28790  wlkf  29551  wlk1ewlk  29577  2wlkdlem6  29865  2wlkond  29871  2trlond  29873  grpofo  30432  vcablo  30502  nvvc  30548  sspba  30660  sspg  30661  minvecolem2  30808  minvecolem4c  30812  minvecolem4  30813  minvecolem5  30814  minvecolem6  30815  eleigveccl  31892  xrofsup  32671  eliccelico  32679  elicoelioo  32680  cyc3evpm  33028  slmdvscl  33078  slmdvsass  33081  imaslmod  33228  prmidlidl  33319  mxidlidl  33338  0ringmon1p  33430  irngss  33563  algextdeglem1  33584  baselsiga  33948  insiga  33970  ldsysgenld  33993  sigapildsys  33995  ldgenpisyslem1  33996  measfrge0  34036  sibfmbl  34169  eulerpartlemt  34205  eulerpartlemmf  34209  probfinmeasbALTV  34263  tg5segofs  34519  pfxwlk  34951  revwlk  34952  subgrwlk  34960  subfacp1lem2a  35008  subfacp1lem2b  35009  subfacp1lem3  35010  subfacp1lem4  35011  subfacp1lem5  35012  sconnpht2  35066  sconnpi1  35067  cvxsconn  35071  cvmlift2lem3  35133  cvmlift2lem5  35135  cvmlift2lem6  35136  cvmlift2lem7  35137  cvmlift2lem12  35142  cvmliftphtlem  35145  cvmliftpht  35146  cvmlift3lem2  35148  cvmlift3lem4  35150  cvmlift3lem5  35151  cvmlift3lem6  35152  msrf  35370  elmsta  35376  mthmpps  35410  mclsppslem  35411  mclspps  35412  iblabsnclem  37384  dvasin  37405  isbnd3  37485  heiborlem3  37514  iccbnd  37541  rngohomf  37667  idlss  37717  lshplss  38679  opoccl  38892  opococ  38893  oplecon3  38897  hloml  39055  lclkrslem1  41236  lclkrslem2  41237  dvrelog2  41763  dvrelog3  41764  aks4d1p1p5  41774  primrootsunit1  41795  primrootscoprmpow  41797  primrootscoprbij  41800  primrootspoweq0  41804  aks6d1c1p2  41807  aks6d1c1p3  41808  aks6d1c1p4  41809  aks6d1c1p5  41810  aks6d1c1p7  41811  aks6d1c1p6  41812  aks6d1c1p8  41813  aks6d1c2lem3  41824  aks6d1c2lem4  41825  aks6d1c2  41828  aks6d1c6lem2  41869  aks6d1c6lem3  41870  aks6d1c6lem4  41871  aks6d1c6isolem1  41872  aks6d1c6isolem2  41873  aks6d1c6lem5  41875  aks5lem1  41884  aks5lem2  41885  aks5lem3a  41887  metakunt8  41898  metakunt19  41909  metakunt21  41911  metakunt22  41912  metakunt25  41915  evlsval3  42031  flt4lem5f  42311  flt4lem7  42313  nna4b4nsq  42314  eliccre  45123  eliocre  45127  icoiccdif  45142  limccog  45241  lptioo1  45253  cncfiooicclem1  45514  ditgeqiooicc  45581  stoweidlem30  45651  stoweidlem31  45652  stoweidlem38  45659  stoweidlem44  45665  fourierdlem26  45754  fourierdlem32  45760  fourierdlem33  45761  fourierdlem37  45765  fourierdlem42  45770  fourierdlem54  45781  fourierdlem63  45790  fourierdlem64  45791  fourierdlem65  45792  fourierdlem69  45796  fourierdlem79  45806  fourierdlem82  45809  fourierdlem89  45816  fourierdlem90  45817  fourierdlem91  45818  fourierdlem111  45838  0sal  45941  hoidmv1lelem3  46214  smfdmss  46354  sigardiv  46482  sigarcol  46485  sharhght  46486  sigaradd  46487  cevathlem1  46488  cevathlem2  46489  cevath  46490  proththd  47186  perfectALTVlem2  47294  isuspgrim0  47451  itsclc0yqsol  48152