Theorem simp1d 1142

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 1136	. 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp1bi  1145  f1dom3fv3dif  7214  f1dom3el3dif  7215  f1prex  7230  oeeui  8530  oeeu  8531  domssex2  9065  domssex  9066  cantnflem1a  9594  cantnflem1b  9595  cantnflem1c  9596  cantnflem1d  9597  cantnflem1  9598  cantnflem3  9600  cantnflem4  9601  fpwwe2lem6  10547  canthnumlem  10559  canthp1lem2  10564  wuntr  10616  lelttrdi  11295  supmul1  12111  supmullem1  12112  supmullem2  12113  supmul  12114  ixxdisj  13276  ixxun  13277  ixxss1  13279  ixxss2  13280  ixxss12  13281  ixxub  13282  ixxlb  13283  iccss2  13333  iocssre  13343  icossre  13344  iccssre  13345  icodisj  13392  iccf1o  13412  xov1plusxeqvd  13414  fzen  13457  intfracq  13779  fldiv  13780  remul  15052  01sqrexlem6  15170  resqrtth  15178  sqrtth  15288  ruclem6  16160  ruclem9  16163  ruclem12  16166  gcdn0cl  16429  crth  16705  phimullem  16706  eulerthlem1  16708  eulerthlem2  16709  pcpremul  16771  prmreclem3  16846  sectcan  17679  sectco  17680  sectmon  17706  monsect  17707  funcf1  17790  funcsect  17796  invfuc  17901  coapm  17995  catciso  18035  psrel  18492  pstr  18500  mhmf  18714  submss  18734  eqger  19107  eqgcpbl  19111  gaorber  19237  orbstafun  19240  cayleyth  19344  dprdgrp  19936  dprdff  19943  ablfac1a  20000  ablfac1b  20001  lmodvscl  20829  lbsss  21029  2idlcpblrng  21226  evlsval3  22044  mpfind  22070  mdetunilem2  22557  mdetunilem5  22560  mdetunilem6  22561  chfacfisfcpmat  22799  cnptop1  23186  lmfpm  23239  lmff  23245  lmcnp  23248  flimtop  23909  tlmtmd  24131  ustssxp  24149  ustdiag  24153  ustfilxp  24157  ustbas2  24169  tusbas  24211  imasdsf1olem  24317  xmeter  24377  tmsbas  24427  metustexhalf  24500  nlmngp  24621  qdensere  24713  blcvx  24742  tgqioo  24744  icccmplem2  24768  reconnlem1  24771  cnmpopc  24878  icoopnst  24892  iocopnst  24893  iccpnfcnv  24898  phtpcer  24950  phtpcco2  24955  pcohtpylem  24975  pcohtpy  24976  pcopt  24978  pcopt2  24979  pcorevlem  24982  pcorev2  24984  pcophtb  24985  om1addcl  24989  pi1grplem  25005  pi1inv  25008  pi1xfrf  25009  pi1xfr  25011  pi1xfrcnvlem  25012  pi1xfrcnv  25013  pi1cof  25015  pi1coghm  25017  cphphl  25127  cphreccllem  25134  cphsqrtcl2  25142  phclm  25188  tcphcph  25193  lmcau  25269  bcthlem4  25283  minveclem4c  25381  minveclem2  25382  minveclem3b  25384  minveclem4  25388  minveclem6  25390  ivthicc  25415  ovolfsval  25427  ovollb2lem  25445  ovolshftlem1  25466  ovolscalem1  25470  ovolicc2lem2  25475  ovolicc2lem5  25478  ovolicopnf  25481  ioombl1lem1  25515  ioombl1lem3  25517  ioombl1lem4  25518  uniioovol  25536  uniioombllem2a  25539  uniioombllem2  25540  uniioombllem3a  25541  uniioombllem3  25542  uniioombllem4  25543  uniioombllem6  25545  vitalilem2  25566  vitalilem3  25567  vitalilem4  25568  i1ff  25633  itg2monolem1  25707  itgreval  25754  ibladd  25778  iblabslem  25785  itgspliticc  25794  itgsplitioo  25795  ditgcl  25815  ditgswap  25816  ditgsplitlem  25817  ditgsplit  25818  limcresi  25842  dvlip2  25956  dveq0  25961  dvcnvre  25980  dvfsumlem2  25989  dvfsumlem2OLD  25990  ftc1a  26000  ply1rem  26127  facth1  26128  fta1glem1  26129  fta1glem2  26130  ig1pcl  26140  ig1pdvds  26141  plyrem  26269  facth  26270  vieta1lem1  26274  vieta1lem2  26275  aaliou3lem3  26308  aaliou3lem7  26313  pserulm  26387  psercnlem2  26390  psercn  26392  pserdvlem1  26393  pserdvlem2  26394  pserdv  26395  abelth2  26408  coseq00topi  26467  coseq0negpitopi  26468  cosordlem  26495  efif1olem1  26507  dvloglem  26613  loglesqrt  26727  relogbval  26738  nnlogbexp  26747  logbrec  26748  quart1  26822  quartlem2  26824  quartlem3  26825  quartlem4  26826  quart  26827  asinsinlem  26857  atanlogsublem  26881  atans2  26897  dvatan  26901  rlimcnp2  26932  divsqrtsumlem  26946  ftalem5  27043  ftalem7  27045  basellem4  27050  basellem5  27051  perfectlem2  27197  dchrinv  27228  chpdifbndlem1  27520  pntibndlem2  27558  pntlema  27563  pntlemb  27564  pntlemg  27565  pntlemh  27566  pntlemn  27567  pntlemq  27568  pntlemr  27569  pntlemj  27570  pntlemf  27572  pntlemk  27573  pntlemo  27574  pntlemp  27577  pntleml  27578  abvcxp  27582  cutscl  27778  cutsun12  27786  ltsrec  27797  addsproplem6  27970  addsprop  27972  addscld  27976  negsproplem6  28029  negsprop  28031  mulsproplem11  28122  mulsproplem12  28123  axtgbtwnid  28538  cgr3simp1  28592  hlne1  28677  hltr  28682  btwnhl  28686  mirhl  28751  opphllem4  28822  hlpasch  28828  inagswap  28913  inagne1  28914  dfcgrg2  28935  wlkf  29688  wlk1ewlk  29713  2wlkdlem6  30004  2wlkond  30010  2trlond  30012  grpofo  30574  vcablo  30644  nvvc  30690  sspba  30802  sspg  30803  minvecolem2  30950  minvecolem4c  30954  minvecolem4  30955  minvecolem5  30956  minvecolem6  30957  eleigveccl  32034  tpssad  32614  xrofsup  32847  eliccelico  32857  elicoelioo  32858  cyc3evpm  33232  slmdvscl  33296  slmdvsass  33299  imaslmod  33434  prmidlidl  33525  mxidlidl  33544  0ringmon1p  33638  irngss  33844  algextdeglem1  33874  constrsqrtcl  33936  baselsiga  34272  insiga  34294  ldsysgenld  34317  sigapildsys  34319  ldgenpisyslem1  34320  measfrge0  34360  sibfmbl  34492  eulerpartlemt  34528  eulerpartlemmf  34532  probfinmeasbALTV  34586  tg5segofs  34830  pfxwlk  35318  revwlk  35319  subgrwlk  35326  subfacp1lem2a  35374  subfacp1lem2b  35375  subfacp1lem3  35376  subfacp1lem4  35377  subfacp1lem5  35378  sconnpht2  35432  sconnpi1  35433  cvxsconn  35437  cvmlift2lem3  35499  cvmlift2lem5  35501  cvmlift2lem6  35502  cvmlift2lem7  35503  cvmlift2lem12  35508  cvmliftphtlem  35511  cvmliftpht  35512  cvmlift3lem2  35514  cvmlift3lem4  35516  cvmlift3lem5  35517  cvmlift3lem6  35518  msrf  35736  elmsta  35742  mthmpps  35776  mclsppslem  35777  mclspps  35778  weiunfrlem  36658  weiunpo  36659  weiunso  36660  weiunfr  36661  weiunse  36662  iblabsnclem  37880  dvasin  37901  isbnd3  37981  heiborlem3  38010  iccbnd  38037  rngohomf  38163  idlss  38213  lshplss  39237  opoccl  39450  opococ  39451  oplecon3  39455  hloml  39613  lclkrslem1  41793  lclkrslem2  41794  dvrelog2  42314  dvrelog3  42315  aks4d1p1p5  42325  primrootsunit1  42347  primrootscoprmpow  42349  primrootscoprbij  42352  primrootspoweq0  42356  aks6d1c1p2  42359  aks6d1c1p3  42360  aks6d1c1p4  42361  aks6d1c1p5  42362  aks6d1c1p7  42363  aks6d1c1p6  42364  aks6d1c1p8  42365  aks6d1c2lem3  42376  aks6d1c2lem4  42377  aks6d1c2  42380  aks6d1c6lem2  42421  aks6d1c6lem3  42422  aks6d1c6lem4  42423  aks6d1c6isolem1  42424  aks6d1c6isolem2  42425  aks6d1c6lem5  42427  aks5lem1  42436  aks5lem2  42437  aks5lem3a  42439  flt4lem5f  42896  flt4lem7  42898  nna4b4nsq  42899  eliccre  45747  eliocre  45751  icoiccdif  45766  limccog  45862  lptioo1  45874  cncfiooicclem1  46133  ditgeqiooicc  46200  stoweidlem30  46270  stoweidlem31  46271  stoweidlem38  46278  stoweidlem44  46284  fourierdlem26  46373  fourierdlem32  46379  fourierdlem33  46380  fourierdlem37  46384  fourierdlem42  46389  fourierdlem54  46400  fourierdlem63  46409  fourierdlem64  46410  fourierdlem65  46411  fourierdlem69  46415  fourierdlem79  46425  fourierdlem82  46428  fourierdlem89  46435  fourierdlem90  46436  fourierdlem91  46437  fourierdlem111  46457  0sal  46560  hoidmv1lelem3  46833  smfdmss  46973  sigardiv  47101  sigarcol  47104  sharhght  47105  sigaradd  47106  cevathlem1  47107  cevathlem2  47108  cevath  47109  nthrucw  47126  proththd  47856  perfectALTVlem2  47964  isuspgrim0  48136  gpgnbgrvtx0  48316  gpgnbgrvtx1  48317  itsclc0yqsol  49006  imaf1hom  49349