Theorem simp1d 1140

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  simp1bi  1143  f1dom3fv3dif  7122  f1dom3el3dif  7123  f1prex  7136  oeeui  8395  oeeu  8396  domssex2  8873  domssex  8874  cantnflem1a  9373  cantnflem1b  9374  cantnflem1c  9375  cantnflem1d  9376  cantnflem1  9377  cantnflem3  9379  cantnflem4  9380  fpwwe2lem6  10323  canthnumlem  10335  canthp1lem2  10340  wuntr  10392  lelttrdi  11067  supmul1  11874  supmullem1  11875  supmullem2  11876  supmul  11877  ixxdisj  13023  ixxun  13024  ixxss1  13026  ixxss2  13027  ixxss12  13028  ixxub  13029  ixxlb  13030  iccss2  13079  iocssre  13088  icossre  13089  iccssre  13090  icodisj  13137  iccf1o  13157  xov1plusxeqvd  13159  fzen  13202  intfracq  13507  fldiv  13508  remul  14768  sqrlem6  14887  resqrtth  14895  sqrtth  15004  ruclem6  15872  ruclem9  15875  ruclem12  15878  gcdn0cl  16137  crth  16407  phimullem  16408  eulerthlem1  16410  eulerthlem2  16411  pcpremul  16472  prmreclem3  16547  sectcan  17384  sectco  17385  sectmon  17411  monsect  17412  funcf1  17497  funcsect  17503  invfuc  17608  coapm  17702  catciso  17742  psrel  18202  pstr  18210  mhmf  18350  submss  18363  eqger  18721  eqgcpbl  18725  gaorber  18829  orbstafun  18832  cayleyth  18938  dprdgrp  19523  dprdff  19530  ablfac1a  19587  ablfac1b  19588  lmodvscl  20055  lbsss  20254  2idlcpbl  20418  assalmod  20977  mpfind  21227  mdetunilem2  21670  mdetunilem5  21673  mdetunilem6  21674  chfacfisfcpmat  21912  cnptop1  22301  lmfpm  22354  lmff  22360  lmcnp  22363  flimtop  23024  tlmtmd  23246  ustssxp  23264  ustdiag  23268  ustfilxp  23272  ustbas2  23285  tusbas  23328  imasdsf1olem  23434  xmeter  23494  tmsbas  23545  metustexhalf  23618  nlmngp  23747  qdensere  23839  blcvx  23867  tgqioo  23869  icccmplem2  23892  reconnlem1  23895  cnmpopc  23997  icoopnst  24008  iocopnst  24009  iccpnfcnv  24013  phtpcer  24064  phtpcco2  24068  pcohtpylem  24088  pcohtpy  24089  pcopt  24091  pcopt2  24092  pcorevlem  24095  pcorev2  24097  pcophtb  24098  om1addcl  24102  pi1grplem  24118  pi1inv  24121  pi1xfrf  24122  pi1xfr  24124  pi1xfrcnvlem  24125  pi1xfrcnv  24126  pi1cof  24128  pi1coghm  24130  cphphl  24240  cphreccllem  24247  cphsqrtcl2  24255  phclm  24301  tcphcph  24306  lmcau  24382  bcthlem4  24396  minveclem4c  24494  minveclem2  24495  minveclem3b  24497  minveclem4  24501  minveclem6  24503  ivthicc  24527  ovolfsval  24539  ovollb2lem  24557  ovolshftlem1  24578  ovolscalem1  24582  ovolicc2lem2  24587  ovolicc2lem5  24590  ovolicopnf  24593  ioombl1lem1  24627  ioombl1lem3  24629  ioombl1lem4  24630  uniioovol  24648  uniioombllem2a  24651  uniioombllem2  24652  uniioombllem3a  24653  uniioombllem3  24654  uniioombllem4  24655  uniioombllem6  24657  vitalilem2  24678  vitalilem3  24679  vitalilem4  24680  i1ff  24745  itg2monolem1  24820  itgreval  24866  ibladd  24890  iblabslem  24897  itgspliticc  24906  itgsplitioo  24907  ditgcl  24927  ditgswap  24928  ditgsplitlem  24929  ditgsplit  24930  limcresi  24954  dvlip2  25064  dveq0  25069  dvcnvre  25088  dvfsumlem2  25096  ftc1a  25106  ply1rem  25233  facth1  25234  fta1glem1  25235  fta1glem2  25236  ig1pcl  25245  ig1pdvds  25246  plyrem  25370  facth  25371  vieta1lem1  25375  vieta1lem2  25376  aaliou3lem3  25409  aaliou3lem7  25414  pserulm  25486  psercnlem2  25488  psercn  25490  pserdvlem1  25491  pserdvlem2  25492  pserdv  25493  abelth2  25506  coseq00topi  25564  coseq0negpitopi  25565  cosordlem  25591  efif1olem1  25603  dvloglem  25708  loglesqrt  25816  relogbval  25827  nnlogbexp  25836  logbrec  25837  quart1  25911  quartlem2  25913  quartlem3  25914  quartlem4  25915  quart  25916  asinsinlem  25946  atanlogsublem  25970  atans2  25986  dvatan  25990  rlimcnp2  26021  divsqrtsumlem  26034  ftalem5  26131  ftalem7  26133  basellem4  26138  basellem5  26139  perfectlem2  26283  dchrinv  26314  chpdifbndlem1  26606  pntibndlem2  26644  pntlema  26649  pntlemb  26650  pntlemg  26651  pntlemh  26652  pntlemn  26653  pntlemq  26654  pntlemr  26655  pntlemj  26656  pntlemf  26658  pntlemk  26659  pntlemo  26660  pntlemp  26663  pntleml  26664  abvcxp  26668  axtgbtwnid  26731  cgr3simp1  26785  hlne1  26870  hltr  26875  btwnhl  26879  mirhl  26944  opphllem4  27015  hlpasch  27021  inagswap  27106  inagne1  27107  dfcgrg2  27128  wlkf  27884  wlk1ewlk  27909  2wlkdlem6  28197  2wlkond  28203  2trlond  28205  grpofo  28762  vcablo  28832  nvvc  28878  sspba  28990  sspg  28991  minvecolem2  29138  minvecolem4c  29142  minvecolem4  29143  minvecolem5  29144  minvecolem6  29145  eleigveccl  30222  xrofsup  30992  eliccelico  31000  elicoelioo  31001  cyc3evpm  31319  slmdvscl  31369  slmdvsass  31372  imaslmod  31455  prmidlidl  31521  mxidlidl  31537  baselsiga  31983  insiga  32005  ldsysgenld  32028  sigapildsys  32030  ldgenpisyslem1  32031  measfrge0  32071  sibfmbl  32202  eulerpartlemt  32238  eulerpartlemmf  32242  probfinmeasbALTV  32296  tg5segofs  32553  pfxwlk  32985  revwlk  32986  subgrwlk  32994  subfacp1lem2a  33042  subfacp1lem2b  33043  subfacp1lem3  33044  subfacp1lem4  33045  subfacp1lem5  33046  sconnpht2  33100  sconnpi1  33101  cvxsconn  33105  cvmlift2lem3  33167  cvmlift2lem5  33169  cvmlift2lem6  33170  cvmlift2lem7  33171  cvmlift2lem12  33176  cvmliftphtlem  33179  cvmliftpht  33180  cvmlift3lem2  33182  cvmlift3lem4  33184  cvmlift3lem5  33185  cvmlift3lem6  33186  msrf  33404  elmsta  33410  mthmpps  33444  mclsppslem  33445  mclspps  33446  scutcl  33923  scutun12  33931  sltrec  33941  iblabsnclem  35767  dvasin  35788  isbnd3  35869  heiborlem3  35898  iccbnd  35925  rngohomf  36051  idlss  36101  lshplss  36922  opoccl  37135  opococ  37136  oplecon3  37140  hloml  37298  lclkrslem1  39478  lclkrslem2  39479  dvrelog2  40000  dvrelog3  40001  aks4d1p1p5  40011  metakunt8  40060  metakunt19  40071  metakunt21  40073  metakunt22  40074  metakunt25  40077  evlsval3  40195  flt4lem5f  40410  flt4lem7  40412  nna4b4nsq  40413  eliccre  42933  eliocre  42937  icoiccdif  42952  limccog  43051  lptioo1  43063  cncfiooicclem1  43324  ditgeqiooicc  43391  stoweidlem30  43461  stoweidlem31  43462  stoweidlem38  43469  stoweidlem44  43475  fourierdlem26  43564  fourierdlem32  43570  fourierdlem33  43571  fourierdlem37  43575  fourierdlem42  43580  fourierdlem54  43591  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem69  43606  fourierdlem79  43616  fourierdlem82  43619  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem111  43648  0sal  43751  hoidmv1lelem3  44021  smfdmss  44156  smfpimltxr  44170  sigardiv  44264  sigarcol  44267  sharhght  44268  sigaradd  44269  cevathlem1  44270  cevathlem2  44271  cevath  44272  proththd  44954  perfectALTVlem2  45062  itsclc0yqsol  45998