Theorem simp1d 1141

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 1135	. 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simp1bi  1144  f1dom3fv3dif  7150  f1dom3el3dif  7151  f1prex  7165  oeeui  8442  oeeu  8443  domssex2  8933  domssex  8934  cantnflem1a  9452  cantnflem1b  9453  cantnflem1c  9454  cantnflem1d  9455  cantnflem1  9456  cantnflem3  9458  cantnflem4  9459  fpwwe2lem6  10401  canthnumlem  10413  canthp1lem2  10418  wuntr  10470  lelttrdi  11146  supmul1  11953  supmullem1  11954  supmullem2  11955  supmul  11956  ixxdisj  13103  ixxun  13104  ixxss1  13106  ixxss2  13107  ixxss12  13108  ixxub  13109  ixxlb  13110  iccss2  13159  iocssre  13168  icossre  13169  iccssre  13170  icodisj  13217  iccf1o  13237  xov1plusxeqvd  13239  fzen  13282  intfracq  13588  fldiv  13589  remul  14849  sqrlem6  14968  resqrtth  14976  sqrtth  15085  ruclem6  15953  ruclem9  15956  ruclem12  15959  gcdn0cl  16218  crth  16488  phimullem  16489  eulerthlem1  16491  eulerthlem2  16492  pcpremul  16553  prmreclem3  16628  sectcan  17476  sectco  17477  sectmon  17503  monsect  17504  funcf1  17590  funcsect  17596  invfuc  17701  coapm  17795  catciso  17835  psrel  18296  pstr  18304  mhmf  18444  submss  18457  eqger  18815  eqgcpbl  18819  gaorber  18923  orbstafun  18926  cayleyth  19032  dprdgrp  19617  dprdff  19624  ablfac1a  19681  ablfac1b  19682  lmodvscl  20149  lbsss  20348  2idlcpbl  20514  assalmod  21076  mpfind  21326  mdetunilem2  21771  mdetunilem5  21774  mdetunilem6  21775  chfacfisfcpmat  22013  cnptop1  22402  lmfpm  22455  lmff  22461  lmcnp  22464  flimtop  23125  tlmtmd  23347  ustssxp  23365  ustdiag  23369  ustfilxp  23373  ustbas2  23386  tusbas  23429  imasdsf1olem  23535  xmeter  23595  tmsbas  23648  metustexhalf  23721  nlmngp  23850  qdensere  23942  blcvx  23970  tgqioo  23972  icccmplem2  23995  reconnlem1  23998  cnmpopc  24100  icoopnst  24111  iocopnst  24112  iccpnfcnv  24116  phtpcer  24167  phtpcco2  24171  pcohtpylem  24191  pcohtpy  24192  pcopt  24194  pcopt2  24195  pcorevlem  24198  pcorev2  24200  pcophtb  24201  om1addcl  24205  pi1grplem  24221  pi1inv  24224  pi1xfrf  24225  pi1xfr  24227  pi1xfrcnvlem  24228  pi1xfrcnv  24229  pi1cof  24231  pi1coghm  24233  cphphl  24344  cphreccllem  24351  cphsqrtcl2  24359  phclm  24405  tcphcph  24410  lmcau  24486  bcthlem4  24500  minveclem4c  24598  minveclem2  24599  minveclem3b  24601  minveclem4  24605  minveclem6  24607  ivthicc  24631  ovolfsval  24643  ovollb2lem  24661  ovolshftlem1  24682  ovolscalem1  24686  ovolicc2lem2  24691  ovolicc2lem5  24694  ovolicopnf  24697  ioombl1lem1  24731  ioombl1lem3  24733  ioombl1lem4  24734  uniioovol  24752  uniioombllem2a  24755  uniioombllem2  24756  uniioombllem3a  24757  uniioombllem3  24758  uniioombllem4  24759  uniioombllem6  24761  vitalilem2  24782  vitalilem3  24783  vitalilem4  24784  i1ff  24849  itg2monolem1  24924  itgreval  24970  ibladd  24994  iblabslem  25001  itgspliticc  25010  itgsplitioo  25011  ditgcl  25031  ditgswap  25032  ditgsplitlem  25033  ditgsplit  25034  limcresi  25058  dvlip2  25168  dveq0  25173  dvcnvre  25192  dvfsumlem2  25200  ftc1a  25210  ply1rem  25337  facth1  25338  fta1glem1  25339  fta1glem2  25340  ig1pcl  25349  ig1pdvds  25350  plyrem  25474  facth  25475  vieta1lem1  25479  vieta1lem2  25480  aaliou3lem3  25513  aaliou3lem7  25518  pserulm  25590  psercnlem2  25592  psercn  25594  pserdvlem1  25595  pserdvlem2  25596  pserdv  25597  abelth2  25610  coseq00topi  25668  coseq0negpitopi  25669  cosordlem  25695  efif1olem1  25707  dvloglem  25812  loglesqrt  25920  relogbval  25931  nnlogbexp  25940  logbrec  25941  quart1  26015  quartlem2  26017  quartlem3  26018  quartlem4  26019  quart  26020  asinsinlem  26050  atanlogsublem  26074  atans2  26090  dvatan  26094  rlimcnp2  26125  divsqrtsumlem  26138  ftalem5  26235  ftalem7  26237  basellem4  26242  basellem5  26243  perfectlem2  26387  dchrinv  26418  chpdifbndlem1  26710  pntibndlem2  26748  pntlema  26753  pntlemb  26754  pntlemg  26755  pntlemh  26756  pntlemn  26757  pntlemq  26758  pntlemr  26759  pntlemj  26760  pntlemf  26762  pntlemk  26763  pntlemo  26764  pntlemp  26767  pntleml  26768  abvcxp  26772  axtgbtwnid  26836  cgr3simp1  26890  hlne1  26975  hltr  26980  btwnhl  26984  mirhl  27049  opphllem4  27120  hlpasch  27126  inagswap  27211  inagne1  27212  dfcgrg2  27233  wlkf  27990  wlk1ewlk  28016  2wlkdlem6  28305  2wlkond  28311  2trlond  28313  grpofo  28870  vcablo  28940  nvvc  28986  sspba  29098  sspg  29099  minvecolem2  29246  minvecolem4c  29250  minvecolem4  29251  minvecolem5  29252  minvecolem6  29253  eleigveccl  30330  xrofsup  31099  eliccelico  31107  elicoelioo  31108  cyc3evpm  31426  slmdvscl  31476  slmdvsass  31479  imaslmod  31562  prmidlidl  31628  mxidlidl  31644  baselsiga  32092  insiga  32114  ldsysgenld  32137  sigapildsys  32139  ldgenpisyslem1  32140  measfrge0  32180  sibfmbl  32311  eulerpartlemt  32347  eulerpartlemmf  32351  probfinmeasbALTV  32405  tg5segofs  32662  pfxwlk  33094  revwlk  33095  subgrwlk  33103  subfacp1lem2a  33151  subfacp1lem2b  33152  subfacp1lem3  33153  subfacp1lem4  33154  subfacp1lem5  33155  sconnpht2  33209  sconnpi1  33210  cvxsconn  33214  cvmlift2lem3  33276  cvmlift2lem5  33278  cvmlift2lem6  33279  cvmlift2lem7  33280  cvmlift2lem12  33285  cvmliftphtlem  33288  cvmliftpht  33289  cvmlift3lem2  33291  cvmlift3lem4  33293  cvmlift3lem5  33294  cvmlift3lem6  33295  msrf  33513  elmsta  33519  mthmpps  33553  mclsppslem  33554  mclspps  33555  scutcl  34005  scutun12  34013  sltrec  34023  iblabsnclem  35849  dvasin  35870  isbnd3  35951  heiborlem3  35980  iccbnd  36007  rngohomf  36133  idlss  36183  lshplss  37002  opoccl  37215  opococ  37216  oplecon3  37220  hloml  37378  lclkrslem1  39558  lclkrslem2  39559  dvrelog2  40079  dvrelog3  40080  aks4d1p1p5  40090  metakunt8  40139  metakunt19  40150  metakunt21  40152  metakunt22  40153  metakunt25  40156  evlsval3  40279  flt4lem5f  40501  flt4lem7  40503  nna4b4nsq  40504  eliccre  43050  eliocre  43054  icoiccdif  43069  limccog  43168  lptioo1  43180  cncfiooicclem1  43441  ditgeqiooicc  43508  stoweidlem30  43578  stoweidlem31  43579  stoweidlem38  43586  stoweidlem44  43592  fourierdlem26  43681  fourierdlem32  43687  fourierdlem33  43688  fourierdlem37  43692  fourierdlem42  43697  fourierdlem54  43708  fourierdlem63  43717  fourierdlem64  43718  fourierdlem65  43719  fourierdlem69  43723  fourierdlem79  43733  fourierdlem82  43736  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem111  43765  0sal  43868  hoidmv1lelem3  44138  smfdmss  44278  sigardiv  44388  sigarcol  44391  sharhght  44392  sigaradd  44393  cevathlem1  44394  cevathlem2  44395  cevath  44396  proththd  45077  perfectALTVlem2  45185  itsclc0yqsol  46121