Theorem simp1d 1138

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp1bi  1141  f1dom3fv3dif  7026  f1dom3el3dif  7027  f1prex  7040  oeeui  8228  oeeu  8229  domssex2  8677  domssex  8678  cantnflem1a  9148  cantnflem1b  9149  cantnflem1c  9150  cantnflem1d  9151  cantnflem1  9152  cantnflem3  9154  cantnflem4  9155  fpwwe2lem7  10058  canthnumlem  10070  canthp1lem2  10075  wuntr  10127  lelttrdi  10802  supmul1  11610  supmullem1  11611  supmullem2  11612  supmul  11613  ixxdisj  12754  ixxun  12755  ixxss1  12757  ixxss2  12758  ixxss12  12759  ixxub  12760  ixxlb  12761  iccss2  12808  iocssre  12817  icossre  12818  iccssre  12819  icodisj  12863  iccf1o  12883  xov1plusxeqvd  12885  fzen  12925  intfracq  13228  fldiv  13229  remul  14488  sqrlem6  14607  resqrtth  14615  sqrtth  14724  ruclem6  15588  ruclem9  15591  ruclem12  15594  gcdn0cl  15851  crth  16115  phimullem  16116  eulerthlem1  16118  eulerthlem2  16119  pcpremul  16180  prmreclem3  16254  sectcan  17025  sectco  17026  sectmon  17052  monsect  17053  funcf1  17136  funcsect  17142  invfuc  17244  coapm  17331  catciso  17367  psrel  17813  pstr  17821  mhmf  17961  submss  17974  eqger  18330  eqgcpbl  18334  gaorber  18438  orbstafun  18441  cayleyth  18543  dprdgrp  19127  dprdff  19134  ablfac1a  19191  ablfac1b  19192  lmodvscl  19651  lbsss  19849  2idlcpbl  20007  assalmod  20092  mpfind  20320  mdetunilem2  21222  mdetunilem5  21225  mdetunilem6  21226  chfacfisfcpmat  21463  cnptop1  21850  lmfpm  21903  lmff  21909  lmcnp  21912  flimtop  22573  tlmtmd  22795  ustssxp  22813  ustdiag  22817  ustfilxp  22821  ustbas2  22834  tusbas  22877  imasdsf1olem  22983  xmeter  23043  tmsbas  23093  metustexhalf  23166  nlmngp  23286  qdensere  23378  blcvx  23406  tgqioo  23408  icccmplem2  23431  reconnlem1  23434  cnmpopc  23532  icoopnst  23543  iocopnst  23544  iccpnfcnv  23548  phtpcer  23599  phtpcco2  23603  pcohtpylem  23623  pcohtpy  23624  pcopt  23626  pcopt2  23627  pcorevlem  23630  pcorev2  23632  pcophtb  23633  om1addcl  23637  pi1grplem  23653  pi1inv  23656  pi1xfrf  23657  pi1xfr  23659  pi1xfrcnvlem  23660  pi1xfrcnv  23661  pi1cof  23663  pi1coghm  23665  cphphl  23775  cphreccllem  23782  cphsqrtcl2  23790  phclm  23835  tcphcph  23840  lmcau  23916  bcthlem4  23930  minveclem4c  24028  minveclem2  24029  minveclem3b  24031  minveclem4  24035  minveclem6  24037  ivthicc  24059  ovolfsval  24071  ovollb2lem  24089  ovolshftlem1  24110  ovolscalem1  24114  ovolicc2lem2  24119  ovolicc2lem5  24122  ovolicopnf  24125  ioombl1lem1  24159  ioombl1lem3  24161  ioombl1lem4  24162  uniioovol  24180  uniioombllem2a  24183  uniioombllem2  24184  uniioombllem3a  24185  uniioombllem3  24186  uniioombllem4  24187  uniioombllem6  24189  vitalilem2  24210  vitalilem3  24211  vitalilem4  24212  i1ff  24277  itg2monolem1  24351  itgreval  24397  ibladd  24421  iblabslem  24428  itgspliticc  24437  itgsplitioo  24438  ditgcl  24456  ditgswap  24457  ditgsplitlem  24458  ditgsplit  24459  limcresi  24483  dvlip2  24592  dveq0  24597  dvcnvre  24616  dvfsumlem2  24624  ftc1a  24634  ply1rem  24757  facth1  24758  fta1glem1  24759  fta1glem2  24760  ig1pcl  24769  ig1pdvds  24770  plyrem  24894  facth  24895  vieta1lem1  24899  vieta1lem2  24900  aaliou3lem3  24933  aaliou3lem7  24938  pserulm  25010  psercnlem2  25012  psercn  25014  pserdvlem1  25015  pserdvlem2  25016  pserdv  25017  abelth2  25030  coseq00topi  25088  coseq0negpitopi  25089  cosordlem  25115  efif1olem1  25126  dvloglem  25231  loglesqrt  25339  relogbval  25350  nnlogbexp  25359  logbrec  25360  quart1  25434  quartlem2  25436  quartlem3  25437  quartlem4  25438  quart  25439  asinsinlem  25469  atanlogsublem  25493  atans2  25509  dvatan  25513  rlimcnp2  25544  divsqrtsumlem  25557  ftalem5  25654  ftalem7  25656  basellem4  25661  basellem5  25662  perfectlem2  25806  dchrinv  25837  chpdifbndlem1  26129  pntibndlem2  26167  pntlema  26172  pntlemb  26173  pntlemg  26174  pntlemh  26175  pntlemn  26176  pntlemq  26177  pntlemr  26178  pntlemj  26179  pntlemf  26181  pntlemk  26182  pntlemo  26183  pntlemp  26186  pntleml  26187  abvcxp  26191  axtgbtwnid  26252  cgr3simp1  26306  hlne1  26391  hltr  26396  btwnhl  26400  mirhl  26465  opphllem4  26536  hlpasch  26542  inagswap  26627  inagne1  26628  dfcgrg2  26649  wlkf  27396  wlk1ewlk  27421  2wlkdlem6  27710  2wlkond  27716  2trlond  27718  grpofo  28276  vcablo  28346  nvvc  28392  sspba  28504  sspg  28505  minvecolem2  28652  minvecolem4c  28656  minvecolem4  28657  minvecolem5  28658  minvecolem6  28659  eleigveccl  29736  xrofsup  30492  eliccelico  30500  elicoelioo  30501  cyc3evpm  30792  slmdvscl  30842  slmdvsass  30845  imaslmod  30922  prmidlidl  30960  mxidlidl  30972  baselsiga  31374  insiga  31396  ldsysgenld  31419  sigapildsys  31421  ldgenpisyslem1  31422  measfrge0  31462  sibfmbl  31593  eulerpartlemt  31629  eulerpartlemmf  31633  probfinmeasbALTV  31687  tg5segofs  31944  pfxwlk  32370  revwlk  32371  subgrwlk  32379  subfacp1lem2a  32427  subfacp1lem2b  32428  subfacp1lem3  32429  subfacp1lem4  32430  subfacp1lem5  32431  sconnpht2  32485  sconnpi1  32486  cvxsconn  32490  cvmlift2lem3  32552  cvmlift2lem5  32554  cvmlift2lem6  32555  cvmlift2lem7  32556  cvmlift2lem12  32561  cvmliftphtlem  32564  cvmliftpht  32565  cvmlift3lem2  32567  cvmlift3lem4  32569  cvmlift3lem5  32570  cvmlift3lem6  32571  msrf  32789  elmsta  32795  mthmpps  32829  mclsppslem  32830  mclspps  32831  scutun12  33271  scutf  33273  slerec  33277  sltrec  33278  madeval2  33290  iblabsnclem  34970  dvasin  34993  isbnd3  35077  heiborlem3  35106  iccbnd  35133  rngohomf  35259  idlss  35309  lshplss  36132  opoccl  36345  opococ  36346  oplecon3  36350  hloml  36508  lclkrslem1  38688  lclkrslem2  38689  eliccre  41830  eliocre  41834  icoiccdif  41849  limccog  41950  lptioo1  41962  cncfiooicclem1  42225  ditgeqiooicc  42294  stoweidlem30  42364  stoweidlem31  42365  stoweidlem38  42372  stoweidlem44  42378  fourierdlem26  42467  fourierdlem32  42473  fourierdlem33  42474  fourierdlem37  42478  fourierdlem42  42483  fourierdlem54  42494  fourierdlem63  42503  fourierdlem64  42504  fourierdlem65  42505  fourierdlem69  42509  fourierdlem79  42519  fourierdlem82  42522  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem111  42551  0sal  42654  hoidmv1lelem3  42924  smfdmss  43059  smfpimltxr  43073  sigardiv  43167  sigarcol  43170  sharhght  43171  sigaradd  43172  cevathlem1  43173  cevathlem2  43174  cevath  43175  proththd  43828  perfectALTVlem2  43936  itsclc0yqsol  44800