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  7260  f1dom3el3dif  7261  f1prex  7276  oeeui  8612  oeeu  8613  domssex2  9149  domssex  9150  cantnflem1a  9697  cantnflem1b  9698  cantnflem1c  9699  cantnflem1d  9700  cantnflem1  9701  cantnflem3  9703  cantnflem4  9704  fpwwe2lem6  10648  canthnumlem  10660  canthp1lem2  10665  wuntr  10717  lelttrdi  11395  supmul1  12209  supmullem1  12210  supmullem2  12211  supmul  12212  ixxdisj  13375  ixxun  13376  ixxss1  13378  ixxss2  13379  ixxss12  13380  ixxub  13381  ixxlb  13382  iccss2  13432  iocssre  13442  icossre  13443  iccssre  13444  icodisj  13491  iccf1o  13511  xov1plusxeqvd  13513  fzen  13556  intfracq  13874  fldiv  13875  remul  15146  01sqrexlem6  15264  resqrtth  15272  sqrtth  15381  ruclem6  16251  ruclem9  16254  ruclem12  16257  gcdn0cl  16519  crth  16795  phimullem  16796  eulerthlem1  16798  eulerthlem2  16799  pcpremul  16861  prmreclem3  16936  sectcan  17766  sectco  17767  sectmon  17793  monsect  17794  funcf1  17877  funcsect  17883  invfuc  17988  coapm  18082  catciso  18122  psrel  18577  pstr  18585  mhmf  18765  submss  18785  eqger  19159  eqgcpbl  19163  gaorber  19289  orbstafun  19292  cayleyth  19394  dprdgrp  19986  dprdff  19993  ablfac1a  20050  ablfac1b  20051  lmodvscl  20833  lbsss  21033  2idlcpblrng  21230  mpfind  22063  mdetunilem2  22549  mdetunilem5  22552  mdetunilem6  22553  chfacfisfcpmat  22791  cnptop1  23178  lmfpm  23231  lmff  23237  lmcnp  23240  flimtop  23901  tlmtmd  24123  ustssxp  24141  ustdiag  24145  ustfilxp  24149  ustbas2  24162  tusbas  24204  imasdsf1olem  24310  xmeter  24370  tmsbas  24420  metustexhalf  24493  nlmngp  24614  qdensere  24706  blcvx  24735  tgqioo  24737  icccmplem2  24761  reconnlem1  24764  cnmpopc  24871  icoopnst  24885  iocopnst  24886  iccpnfcnv  24891  phtpcer  24943  phtpcco2  24948  pcohtpylem  24968  pcohtpy  24969  pcopt  24971  pcopt2  24972  pcorevlem  24975  pcorev2  24977  pcophtb  24978  om1addcl  24982  pi1grplem  24998  pi1inv  25001  pi1xfrf  25002  pi1xfr  25004  pi1xfrcnvlem  25005  pi1xfrcnv  25006  pi1cof  25008  pi1coghm  25010  cphphl  25121  cphreccllem  25128  cphsqrtcl2  25136  phclm  25182  tcphcph  25187  lmcau  25263  bcthlem4  25277  minveclem4c  25375  minveclem2  25376  minveclem3b  25378  minveclem4  25382  minveclem6  25384  ivthicc  25409  ovolfsval  25421  ovollb2lem  25439  ovolshftlem1  25460  ovolscalem1  25464  ovolicc2lem2  25469  ovolicc2lem5  25472  ovolicopnf  25475  ioombl1lem1  25509  ioombl1lem3  25511  ioombl1lem4  25512  uniioovol  25530  uniioombllem2a  25533  uniioombllem2  25534  uniioombllem3a  25535  uniioombllem3  25536  uniioombllem4  25537  uniioombllem6  25539  vitalilem2  25560  vitalilem3  25561  vitalilem4  25562  i1ff  25627  itg2monolem1  25701  itgreval  25748  ibladd  25772  iblabslem  25779  itgspliticc  25788  itgsplitioo  25789  ditgcl  25809  ditgswap  25810  ditgsplitlem  25811  ditgsplit  25812  limcresi  25836  dvlip2  25950  dveq0  25955  dvcnvre  25974  dvfsumlem2  25983  dvfsumlem2OLD  25984  ftc1a  25994  ply1rem  26121  facth1  26122  fta1glem1  26123  fta1glem2  26124  ig1pcl  26134  ig1pdvds  26135  plyrem  26263  facth  26264  vieta1lem1  26268  vieta1lem2  26269  aaliou3lem3  26302  aaliou3lem7  26307  pserulm  26381  psercnlem2  26384  psercn  26386  pserdvlem1  26387  pserdvlem2  26388  pserdv  26389  abelth2  26402  coseq00topi  26461  coseq0negpitopi  26462  cosordlem  26489  efif1olem1  26501  dvloglem  26607  loglesqrt  26721  relogbval  26732  nnlogbexp  26741  logbrec  26742  quart1  26816  quartlem2  26818  quartlem3  26819  quartlem4  26820  quart  26821  asinsinlem  26851  atanlogsublem  26875  atans2  26891  dvatan  26895  rlimcnp2  26926  divsqrtsumlem  26940  ftalem5  27037  ftalem7  27039  basellem4  27044  basellem5  27045  perfectlem2  27191  dchrinv  27222  chpdifbndlem1  27514  pntibndlem2  27552  pntlema  27557  pntlemb  27558  pntlemg  27559  pntlemh  27560  pntlemn  27561  pntlemq  27562  pntlemr  27563  pntlemj  27564  pntlemf  27566  pntlemk  27567  pntlemo  27568  pntlemp  27571  pntleml  27572  abvcxp  27576  scutcl  27764  scutun12  27772  sltrec  27782  addsproplem6  27924  addsprop  27926  addscld  27930  negsproplem6  27982  negsprop  27984  mulsproplem11  28069  mulsproplem12  28070  axtgbtwnid  28391  cgr3simp1  28445  hlne1  28530  hltr  28535  btwnhl  28539  mirhl  28604  opphllem4  28675  hlpasch  28681  inagswap  28766  inagne1  28767  dfcgrg2  28788  wlkf  29540  wlk1ewlk  29566  2wlkdlem6  29859  2wlkond  29865  2trlond  29867  grpofo  30426  vcablo  30496  nvvc  30542  sspba  30654  sspg  30655  minvecolem2  30802  minvecolem4c  30806  minvecolem4  30807  minvecolem5  30808  minvecolem6  30809  eleigveccl  31886  tpssad  32466  xrofsup  32690  eliccelico  32700  elicoelioo  32701  cyc3evpm  33107  slmdvscl  33157  slmdvsass  33160  imaslmod  33314  prmidlidl  33405  mxidlidl  33424  0ringmon1p  33516  irngss  33674  algextdeglem1  33697  constrsqrtcl  33759  baselsiga  34092  insiga  34114  ldsysgenld  34137  sigapildsys  34139  ldgenpisyslem1  34140  measfrge0  34180  sibfmbl  34313  eulerpartlemt  34349  eulerpartlemmf  34353  probfinmeasbALTV  34407  tg5segofs  34651  pfxwlk  35092  revwlk  35093  subgrwlk  35100  subfacp1lem2a  35148  subfacp1lem2b  35149  subfacp1lem3  35150  subfacp1lem4  35151  subfacp1lem5  35152  sconnpht2  35206  sconnpi1  35207  cvxsconn  35211  cvmlift2lem3  35273  cvmlift2lem5  35275  cvmlift2lem6  35276  cvmlift2lem7  35277  cvmlift2lem12  35282  cvmliftphtlem  35285  cvmliftpht  35286  cvmlift3lem2  35288  cvmlift3lem4  35290  cvmlift3lem5  35291  cvmlift3lem6  35292  msrf  35510  elmsta  35516  mthmpps  35550  mclsppslem  35551  mclspps  35552  weiunfrlem  36428  weiunpo  36429  weiunso  36430  weiunfr  36431  weiunse  36432  iblabsnclem  37653  dvasin  37674  isbnd3  37754  heiborlem3  37783  iccbnd  37810  rngohomf  37936  idlss  37986  lshplss  38945  opoccl  39158  opococ  39159  oplecon3  39163  hloml  39321  lclkrslem1  41502  lclkrslem2  41503  dvrelog2  42023  dvrelog3  42024  aks4d1p1p5  42034  primrootsunit1  42056  primrootscoprmpow  42058  primrootscoprbij  42061  primrootspoweq0  42065  aks6d1c1p2  42068  aks6d1c1p3  42069  aks6d1c1p4  42070  aks6d1c1p5  42071  aks6d1c1p7  42072  aks6d1c1p6  42073  aks6d1c1p8  42074  aks6d1c2lem3  42085  aks6d1c2lem4  42086  aks6d1c2  42089  aks6d1c6lem2  42130  aks6d1c6lem3  42131  aks6d1c6lem4  42132  aks6d1c6isolem1  42133  aks6d1c6isolem2  42134  aks6d1c6lem5  42136  aks5lem1  42145  aks5lem2  42146  aks5lem3a  42148  metakunt8  42171  metakunt19  42182  metakunt21  42184  metakunt22  42185  metakunt25  42188  evlsval3  42529  flt4lem5f  42627  flt4lem7  42629  nna4b4nsq  42630  eliccre  45482  eliocre  45486  icoiccdif  45501  limccog  45597  lptioo1  45609  cncfiooicclem1  45870  ditgeqiooicc  45937  stoweidlem30  46007  stoweidlem31  46008  stoweidlem38  46015  stoweidlem44  46021  fourierdlem26  46110  fourierdlem32  46116  fourierdlem33  46117  fourierdlem37  46121  fourierdlem42  46126  fourierdlem54  46137  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem69  46152  fourierdlem79  46162  fourierdlem82  46165  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem111  46194  0sal  46297  hoidmv1lelem3  46570  smfdmss  46710  sigardiv  46838  sigarcol  46841  sharhght  46842  sigaradd  46843  cevathlem1  46844  cevathlem2  46845  cevath  46846  proththd  47576  perfectALTVlem2  47684  isuspgrim0  47855  gpgnbgrvtx0  48024  gpgnbgrvtx1  48025  itsclc0yqsol  48692  imaf1hom  49015