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 210  df-an 400  df-3an 1086

This theorem is referenced by:  simp1bi  1142  f1dom3fv3dif  7004  f1dom3el3dif  7005  f1prex  7018  oeeui  8211  oeeu  8212  domssex2  8661  domssex  8662  cantnflem1a  9132  cantnflem1b  9133  cantnflem1c  9134  cantnflem1d  9135  cantnflem1  9136  cantnflem3  9138  cantnflem4  9139  fpwwe2lem7  10047  canthnumlem  10059  canthp1lem2  10064  wuntr  10116  lelttrdi  10791  supmul1  11597  supmullem1  11598  supmullem2  11599  supmul  11600  ixxdisj  12741  ixxun  12742  ixxss1  12744  ixxss2  12745  ixxss12  12746  ixxub  12747  ixxlb  12748  iccss2  12796  iocssre  12805  icossre  12806  iccssre  12807  icodisj  12854  iccf1o  12874  xov1plusxeqvd  12876  fzen  12919  intfracq  13222  fldiv  13223  remul  14480  sqrlem6  14599  resqrtth  14607  sqrtth  14716  ruclem6  15580  ruclem9  15583  ruclem12  15586  gcdn0cl  15841  crth  16105  phimullem  16106  eulerthlem1  16108  eulerthlem2  16109  pcpremul  16170  prmreclem3  16244  sectcan  17017  sectco  17018  sectmon  17044  monsect  17045  funcf1  17128  funcsect  17134  invfuc  17236  coapm  17323  catciso  17359  psrel  17805  pstr  17813  mhmf  17953  submss  17966  eqger  18322  eqgcpbl  18326  gaorber  18430  orbstafun  18433  cayleyth  18535  dprdgrp  19120  dprdff  19127  ablfac1a  19184  ablfac1b  19185  lmodvscl  19644  lbsss  19842  2idlcpbl  20000  assalmod  20549  mpfind  20779  mdetunilem2  21218  mdetunilem5  21221  mdetunilem6  21222  chfacfisfcpmat  21460  cnptop1  21847  lmfpm  21900  lmff  21906  lmcnp  21909  flimtop  22570  tlmtmd  22792  ustssxp  22810  ustdiag  22814  ustfilxp  22818  ustbas2  22831  tusbas  22874  imasdsf1olem  22980  xmeter  23040  tmsbas  23090  metustexhalf  23163  nlmngp  23283  qdensere  23375  blcvx  23403  tgqioo  23405  icccmplem2  23428  reconnlem1  23431  cnmpopc  23533  icoopnst  23544  iocopnst  23545  iccpnfcnv  23549  phtpcer  23600  phtpcco2  23604  pcohtpylem  23624  pcohtpy  23625  pcopt  23627  pcopt2  23628  pcorevlem  23631  pcorev2  23633  pcophtb  23634  om1addcl  23638  pi1grplem  23654  pi1inv  23657  pi1xfrf  23658  pi1xfr  23660  pi1xfrcnvlem  23661  pi1xfrcnv  23662  pi1cof  23664  pi1coghm  23666  cphphl  23776  cphreccllem  23783  cphsqrtcl2  23791  phclm  23836  tcphcph  23841  lmcau  23917  bcthlem4  23931  minveclem4c  24029  minveclem2  24030  minveclem3b  24032  minveclem4  24036  minveclem6  24038  ivthicc  24062  ovolfsval  24074  ovollb2lem  24092  ovolshftlem1  24113  ovolscalem1  24117  ovolicc2lem2  24122  ovolicc2lem5  24125  ovolicopnf  24128  ioombl1lem1  24162  ioombl1lem3  24164  ioombl1lem4  24165  uniioovol  24183  uniioombllem2a  24186  uniioombllem2  24187  uniioombllem3a  24188  uniioombllem3  24189  uniioombllem4  24190  uniioombllem6  24192  vitalilem2  24213  vitalilem3  24214  vitalilem4  24215  i1ff  24280  itg2monolem1  24354  itgreval  24400  ibladd  24424  iblabslem  24431  itgspliticc  24440  itgsplitioo  24441  ditgcl  24461  ditgswap  24462  ditgsplitlem  24463  ditgsplit  24464  limcresi  24488  dvlip2  24598  dveq0  24603  dvcnvre  24622  dvfsumlem2  24630  ftc1a  24640  ply1rem  24764  facth1  24765  fta1glem1  24766  fta1glem2  24767  ig1pcl  24776  ig1pdvds  24777  plyrem  24901  facth  24902  vieta1lem1  24906  vieta1lem2  24907  aaliou3lem3  24940  aaliou3lem7  24945  pserulm  25017  psercnlem2  25019  psercn  25021  pserdvlem1  25022  pserdvlem2  25023  pserdv  25024  abelth2  25037  coseq00topi  25095  coseq0negpitopi  25096  cosordlem  25122  efif1olem1  25134  dvloglem  25239  loglesqrt  25347  relogbval  25358  nnlogbexp  25367  logbrec  25368  quart1  25442  quartlem2  25444  quartlem3  25445  quartlem4  25446  quart  25447  asinsinlem  25477  atanlogsublem  25501  atans2  25517  dvatan  25521  rlimcnp2  25552  divsqrtsumlem  25565  ftalem5  25662  ftalem7  25664  basellem4  25669  basellem5  25670  perfectlem2  25814  dchrinv  25845  chpdifbndlem1  26137  pntibndlem2  26175  pntlema  26180  pntlemb  26181  pntlemg  26182  pntlemh  26183  pntlemn  26184  pntlemq  26185  pntlemr  26186  pntlemj  26187  pntlemf  26189  pntlemk  26190  pntlemo  26191  pntlemp  26194  pntleml  26195  abvcxp  26199  axtgbtwnid  26260  cgr3simp1  26314  hlne1  26399  hltr  26404  btwnhl  26408  mirhl  26473  opphllem4  26544  hlpasch  26550  inagswap  26635  inagne1  26636  dfcgrg2  26657  wlkf  27404  wlk1ewlk  27429  2wlkdlem6  27717  2wlkond  27723  2trlond  27725  grpofo  28282  vcablo  28352  nvvc  28398  sspba  28510  sspg  28511  minvecolem2  28658  minvecolem4c  28662  minvecolem4  28663  minvecolem5  28664  minvecolem6  28665  eleigveccl  29742  xrofsup  30518  eliccelico  30526  elicoelioo  30527  cyc3evpm  30842  slmdvscl  30892  slmdvsass  30895  imaslmod  30973  prmidlidl  31027  mxidlidl  31043  baselsiga  31484  insiga  31506  ldsysgenld  31529  sigapildsys  31531  ldgenpisyslem1  31532  measfrge0  31572  sibfmbl  31703  eulerpartlemt  31739  eulerpartlemmf  31743  probfinmeasbALTV  31797  tg5segofs  32054  pfxwlk  32483  revwlk  32484  subgrwlk  32492  subfacp1lem2a  32540  subfacp1lem2b  32541  subfacp1lem3  32542  subfacp1lem4  32543  subfacp1lem5  32544  sconnpht2  32598  sconnpi1  32599  cvxsconn  32603  cvmlift2lem3  32665  cvmlift2lem5  32667  cvmlift2lem6  32668  cvmlift2lem7  32669  cvmlift2lem12  32674  cvmliftphtlem  32677  cvmliftpht  32678  cvmlift3lem2  32680  cvmlift3lem4  32682  cvmlift3lem5  32683  cvmlift3lem6  32684  msrf  32902  elmsta  32908  mthmpps  32942  mclsppslem  32943  mclspps  32944  scutun12  33384  scutf  33386  slerec  33390  sltrec  33391  madeval2  33403  iblabsnclem  35120  dvasin  35141  isbnd3  35222  heiborlem3  35251  iccbnd  35278  rngohomf  35404  idlss  35454  lshplss  36277  opoccl  36490  opococ  36491  oplecon3  36495  hloml  36653  lclkrslem1  38833  lclkrslem2  38834  metakunt8  39357  metakunt19  39368  metakunt21  39370  metakunt22  39371  metakunt25  39374  eliccre  42142  eliocre  42146  icoiccdif  42161  limccog  42262  lptioo1  42274  cncfiooicclem1  42535  ditgeqiooicc  42602  stoweidlem30  42672  stoweidlem31  42673  stoweidlem38  42680  stoweidlem44  42686  fourierdlem26  42775  fourierdlem32  42781  fourierdlem33  42782  fourierdlem37  42786  fourierdlem42  42791  fourierdlem54  42802  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem69  42817  fourierdlem79  42827  fourierdlem82  42830  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem111  42859  0sal  42962  hoidmv1lelem3  43232  smfdmss  43367  smfpimltxr  43381  sigardiv  43475  sigarcol  43478  sharhght  43479  sigaradd  43480  cevathlem1  43481  cevathlem2  43482  cevath  43483  proththd  44132  perfectALTVlem2  44240  itsclc0yqsol  45178