Theorem simp1d 1123

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

Syntax hints:   → wi 4   ∧ w3a 1069

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 199  df-an 388  df-3an 1071

This theorem is referenced by:  simp1bi  1126  f1dom3fv3dif  6850  f1dom3el3dif  6851  f1prex  6864  oeeui  8028  oeeu  8029  domssex2  8472  domssex  8473  cantnflem1a  8941  cantnflem1b  8942  cantnflem1c  8943  cantnflem1d  8944  cantnflem1  8945  cantnflem3  8947  cantnflem4  8948  fpwwe2lem7  9855  canthnumlem  9867  canthp1lem2  9872  wuntr  9924  lelttrdi  10601  supmul1  11410  supmullem1  11411  supmullem2  11412  supmul  11413  ixxdisj  12568  ixxun  12569  ixxss1  12571  ixxss2  12572  ixxss12  12573  ixxub  12574  ixxlb  12575  iccss2  12622  iocssre  12631  icossre  12632  iccssre  12633  icodisj  12677  iccf1o  12697  xov1plusxeqvd  12699  fzen  12739  intfracq  13041  fldiv  13042  remul  14348  sqrlem6  14467  resqrtth  14475  sqrtth  14584  ruclem6  15447  ruclem9  15450  ruclem12  15453  gcdn0cl  15710  crth  15970  phimullem  15971  eulerthlem1  15973  eulerthlem2  15974  pcpremul  16035  prmreclem3  16109  sectcan  16896  sectco  16897  sectmon  16923  monsect  16924  funcf1  17007  funcsect  17013  invfuc  17115  coapm  17202  catciso  17238  psrel  17684  pstr  17692  mhmf  17821  submss  17831  eqger  18126  eqgcpbl  18130  gaorber  18222  orbstafun  18225  cayleyth  18317  dprdgrp  18890  dprdff  18897  ablfac1a  18954  ablfac1b  18955  lmodvscl  19386  lbsss  19584  2idlcpbl  19741  assalmod  19826  mpfind  20042  mdetunilem2  20942  mdetunilem5  20945  mdetunilem6  20946  chfacfisfcpmat  21183  cnptop1  21570  lmfpm  21623  lmff  21629  lmcnp  21632  flimtop  22293  tlmtmd  22514  ustssxp  22532  ustdiag  22536  ustfilxp  22540  ustbas2  22553  tusbas  22596  imasdsf1olem  22702  xmeter  22762  tmsbas  22812  metustexhalf  22885  nlmngp  23005  qdensere  23097  blcvx  23125  tgqioo  23127  icccmplem2  23150  reconnlem1  23153  cnmpopc  23251  icoopnst  23262  iocopnst  23263  iccpnfcnv  23267  phtpcer  23318  phtpcco2  23322  pcohtpylem  23342  pcohtpy  23343  pcopt  23345  pcopt2  23346  pcorevlem  23349  pcorev2  23351  pcophtb  23352  om1addcl  23356  pi1grplem  23372  pi1inv  23375  pi1xfrf  23376  pi1xfr  23378  pi1xfrcnvlem  23379  pi1xfrcnv  23380  pi1cof  23382  pi1coghm  23384  cphphl  23494  cphreccllem  23501  cphsqrtcl2  23509  phclm  23554  tcphcph  23559  lmcau  23635  bcthlem4  23649  minveclem4c  23747  minveclem2  23748  minveclem3b  23750  minveclem4  23754  minveclem6  23756  ivthicc  23778  ovolfsval  23790  ovollb2lem  23808  ovolshftlem1  23829  ovolscalem1  23833  ovolicc2lem2  23838  ovolicc2lem5  23841  ovolicopnf  23844  ioombl1lem1  23878  ioombl1lem3  23880  ioombl1lem4  23881  uniioovol  23899  uniioombllem2a  23902  uniioombllem2  23903  uniioombllem3a  23904  uniioombllem3  23905  uniioombllem4  23906  uniioombllem6  23908  vitalilem2  23929  vitalilem3  23930  vitalilem4  23931  i1ff  23996  itg2monolem1  24070  itgreval  24116  ibladd  24140  iblabslem  24147  itgspliticc  24156  itgsplitioo  24157  ditgcl  24175  ditgswap  24176  ditgsplitlem  24177  ditgsplit  24178  limcresi  24202  dvlip2  24311  dveq0  24316  dvcnvre  24335  dvfsumlem2  24343  ftc1a  24353  ply1rem  24476  facth1  24477  fta1glem1  24478  fta1glem2  24479  ig1pcl  24488  ig1pdvds  24489  plyrem  24613  facth  24614  vieta1lem1  24618  vieta1lem2  24619  aaliou3lem3  24652  aaliou3lem7  24657  pserulm  24729  psercnlem2  24731  psercn  24733  pserdvlem1  24734  pserdvlem2  24735  pserdv  24736  abelth2  24749  coseq00topi  24807  coseq0negpitopi  24808  cosordlem  24832  efif1olem1  24843  dvloglem  24948  loglesqrt  25056  relogbval  25067  nnlogbexp  25076  logbrec  25077  quart1  25151  quartlem2  25153  quartlem3  25154  quartlem4  25155  quart  25156  asinsinlem  25186  atanlogsublem  25210  atans2  25226  dvatan  25230  rlimcnp2  25262  divsqrtsumlem  25275  ftalem5  25372  ftalem7  25374  basellem4  25379  basellem5  25380  perfectlem2  25524  dchrinv  25555  chpdifbndlem1  25847  pntibndlem2  25885  pntlema  25890  pntlemb  25891  pntlemg  25892  pntlemh  25893  pntlemn  25894  pntlemq  25895  pntlemr  25896  pntlemj  25897  pntlemf  25899  pntlemk  25900  pntlemo  25901  pntlemp  25904  pntleml  25905  abvcxp  25909  axtgbtwnid  25970  cgr3simp1  26024  hlne1  26109  hltr  26114  btwnhl  26118  mirhl  26183  opphllem4  26254  hlpasch  26260  inagswap  26346  inagne1  26347  dfcgrg2  26368  wlkf  27115  wlk1ewlk  27140  2wlkdlem6  27453  2wlkond  27459  2trlond  27461  grpofo  28069  vcablo  28139  nvvc  28185  sspba  28297  sspg  28298  minvecolem2  28446  minvecolem4c  28450  minvecolem4  28451  minvecolem5  28452  minvecolem6  28453  eleigveccl  29533  xrofsup  30269  eliccelico  30277  elicoelioo  30278  cyc3evpm  30496  slmdvscl  30541  slmdvsass  30544  imaslmod  30634  baselsiga  31052  insiga  31074  ldsysgenld  31097  sigapildsys  31099  ldgenpisyslem1  31100  measfrge0  31140  sibfmbl  31271  eulerpartlemt  31307  eulerpartlemmf  31311  probfinmeasbOLD  31365  tg5segofs  31625  subfacp1lem2a  32045  subfacp1lem2b  32046  subfacp1lem3  32047  subfacp1lem4  32048  subfacp1lem5  32049  sconnpht2  32103  sconnpi1  32104  cvxsconn  32108  cvmlift2lem3  32170  cvmlift2lem5  32172  cvmlift2lem6  32173  cvmlift2lem7  32174  cvmlift2lem12  32179  cvmliftphtlem  32182  cvmliftpht  32183  cvmlift3lem2  32185  cvmlift3lem4  32187  cvmlift3lem5  32188  cvmlift3lem6  32189  msrf  32342  elmsta  32348  mthmpps  32382  mclsppslem  32383  mclspps  32384  scutun12  32825  scutf  32827  slerec  32831  sltrec  32832  madeval2  32844  iblabsnclem  34429  dvasin  34452  isbnd3  34537  heiborlem3  34566  iccbnd  34593  rngohomf  34719  idlss  34769  lshplss  35595  opoccl  35808  opococ  35809  oplecon3  35813  hloml  35971  lclkrslem1  38151  lclkrslem2  38152  eliccre  41242  eliocre  41246  icoiccdif  41261  limccog  41362  lptioo1  41374  cncfiooicclem1  41636  ditgeqiooicc  41705  stoweidlem30  41776  stoweidlem31  41777  stoweidlem38  41784  stoweidlem44  41790  fourierdlem26  41879  fourierdlem32  41885  fourierdlem33  41886  fourierdlem37  41890  fourierdlem42  41895  fourierdlem54  41906  fourierdlem63  41915  fourierdlem64  41916  fourierdlem65  41917  fourierdlem69  41921  fourierdlem79  41931  fourierdlem82  41934  fourierdlem89  41941  fourierdlem90  41942  fourierdlem91  41943  fourierdlem111  41963  0sal  42066  hoidmv1lelem3  42336  smfdmss  42471  smfpimltxr  42485  sigardiv  42579  sigarcol  42582  sharhght  42583  sigaradd  42584  cevathlem1  42585  cevathlem2  42586  cevath  42587  proththd  43177  perfectALTVlem2  43285  itsclc0yqsol  44149