Theorem simp1d 1158

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  simp1bi  1161  f1dom3fv3dif  7256  f1dom3el3dif  7257  f1prex  7272  oeeui  8576  oeeu  8577  domssex2  9113  domssex  9114  cantnflem1a  9642  cantnflem1b  9643  cantnflem1c  9644  cantnflem1d  9645  cantnflem1  9646  cantnflem3  9648  cantnflem4  9649  fpwwe2lem6  10609  canthnumlem  10621  canthp1lem2  10626  wuntr  10678  lelttrdi  11360  supmul1  12172  supmullem1  12173  supmullem2  12174  supmul  12175  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  13557  intfracq  13880  fldiv  13881  remul  15168  01sqrexlem6  15286  resqrtth  15294  sqrtth  15404  ruclem6  16279  ruclem9  16282  ruclem12  16285  gcdn0cl  16548  crth  16825  phimullem  16826  eulerthlem1  16828  eulerthlem2  16829  pcpremul  16891  prmreclem3  16966  sectcan  17800  sectco  17801  sectmon  17827  monsect  17828  funcf1  17911  funcsect  17917  invfuc  18022  coapm  18116  catciso  18156  psrel  18613  pstr  18621  mhmf  18835  submss  18855  eqger  19234  eqgcpbl  19238  gaorber  19366  orbstafun  19369  cayleyth  19473  dprdgrp  20065  dprdff  20072  ablfac1a  20129  ablfac1b  20130  lmodvscl  20965  lbsss  21164  2idlcpblrng  21369  prmidlidl  21428  evlsval3  22197  mpfind  22223  mdetunilem2  22727  mdetunilem5  22730  mdetunilem6  22731  chfacfisfcpmat  22969  cnptop1  23356  lmfpm  23409  lmff  23415  lmcnp  23418  flimtop  24079  tlmtmd  24301  ustssxp  24319  ustdiag  24323  ustfilxp  24327  ustbas2  24339  tusbas  24381  imasdsf1olem  24487  xmeter  24547  tmsbas  24597  metustexhalf  24670  nlmngp  24791  qdensere  24883  blcvx  24912  tgqioo  24914  icccmplem2  24938  reconnlem1  24941  cnmpopc  25044  icoopnst  25055  iocopnst  25056  iccpnfcnv  25060  phtpcer  25111  phtpcco2  25115  pcohtpylem  25135  pcohtpy  25136  pcopt  25138  pcopt2  25139  pcorevlem  25142  pcorev2  25144  pcophtb  25145  om1addcl  25149  pi1grplem  25165  pi1inv  25168  pi1xfrf  25169  pi1xfr  25171  pi1xfrcnvlem  25172  pi1xfrcnv  25173  pi1cof  25175  pi1coghm  25177  cphphl  25287  cphreccllem  25294  cphsqrtcl2  25302  phclm  25348  tcphcph  25353  lmcau  25429  bcthlem4  25443  minveclem4c  25541  minveclem2  25542  minveclem3b  25544  minveclem4  25548  minveclem6  25550  ivthicc  25574  ovolfsval  25586  ovollb2lem  25604  ovolshftlem1  25625  ovolscalem1  25629  ovolicc2lem2  25634  ovolicc2lem5  25637  ovolicopnf  25640  ioombl1lem1  25674  ioombl1lem3  25676  ioombl1lem4  25677  uniioovol  25695  uniioombllem2a  25698  uniioombllem2  25699  uniioombllem3a  25700  uniioombllem3  25701  uniioombllem4  25702  uniioombllem6  25704  vitalilem2  25725  vitalilem3  25726  vitalilem4  25727  i1ff  25792  itg2monolem1  25866  itgreval  25913  ibladd  25937  iblabslem  25944  itgspliticc  25953  itgsplitioo  25954  ditgcl  25974  ditgswap  25975  ditgsplitlem  25976  ditgsplit  25977  limcresi  26001  dvlip2  26111  dveq0  26116  dvcnvre  26135  dvfsumlem2  26143  ftc1a  26153  ply1rem  26280  facth1  26281  fta1glem1  26282  fta1glem2  26283  ig1pcl  26293  ig1pdvds  26294  plyrem  26423  facth  26424  vieta1lem1  26428  vieta1lem2  26429  aaliou3lem3  26462  aaliou3lem7  26467  pserulm  26539  psercnlem2  26541  psercn  26543  pserdvlem1  26544  pserdvlem2  26545  pserdv  26546  abelth2  26559  coseq00topi  26621  coseq0negpitopi  26622  cosordlem  26649  efif1olem1  26661  dvloglem  26767  loglesqrt  26880  relogbval  26891  nnlogbexp  26900  logbrec  26901  quart1  26975  quartlem2  26977  quartlem3  26978  quartlem4  26979  quart  26980  asinsinlem  27010  atanlogsublem  27034  atans2  27050  dvatan  27054  rlimcnp2  27085  divsqrtsumlem  27098  ftalem5  27195  ftalem7  27197  basellem4  27202  basellem5  27203  perfectlem2  27348  dchrinv  27379  chpdifbndlem1  27671  pntibndlem2  27709  pntlema  27714  pntlemb  27715  pntlemg  27716  pntlemh  27717  pntlemn  27718  pntlemq  27719  pntlemr  27720  pntlemj  27721  pntlemf  27723  pntlemk  27724  pntlemo  27725  pntlemp  27728  pntleml  27729  abvcxp  27733  cutscl  27929  cutsun12  27937  ltsrec  27948  addsproplem6  28121  addsprop  28123  addscld  28127  negsproplem6  28180  negsprop  28182  mulsproplem11  28273  mulsproplem12  28274  axtgbtwnid  28689  cgr3simp1  28743  hlne1  28828  hltr  28833  btwnhl  28837  mirhl  28906  opphllem4  28977  hlpasch  28983  inagswap  29089  inagne1  29090  dfcgrg2  29111  wlkf  29869  wlk1ewlk  29894  2wlkdlem6  30185  2wlkond  30191  2trlond  30193  grpofo  30756  vcablo  30826  nvvc  30872  sspba  30984  sspg  30985  minvecolem2  31132  minvecolem4c  31136  minvecolem4  31137  minvecolem5  31138  minvecolem6  31139  eleigveccl  32216  tpssad  32791  xrofsup  33020  eliccelico  33030  elicoelioo  33031  cyc3evpm  33378  slmdvscl  33442  slmdvsass  33445  imaslmod  33583  mxidlidl  33658  0ringmon1p  33759  irngss  33989  algextdeglem1  34019  constrsqrtcl  34081  baselsiga  34417  insiga  34439  ldsysgenld  34462  sigapildsys  34464  ldgenpisyslem1  34465  measfrge0  34505  sibfmbl  34637  eulerpartlemt  34673  eulerpartlemmf  34677  probfinmeasbALTV  34731  tg5segofs  34975  pfxwlk  35482  revwlk  35483  subgrwlk  35490  subfacp1lem2a  35538  subfacp1lem2b  35539  subfacp1lem3  35540  subfacp1lem4  35541  subfacp1lem5  35542  sconnpht2  35596  sconnpi1  35597  cvxsconn  35601  cvmlift2lem3  35663  cvmlift2lem5  35665  cvmlift2lem6  35666  cvmlift2lem7  35667  cvmlift2lem12  35672  cvmliftphtlem  35675  cvmliftpht  35676  cvmlift3lem2  35678  cvmlift3lem4  35680  cvmlift3lem5  35681  cvmlift3lem6  35682  msrf  35900  elmsta  35906  mthmpps  35940  mclsppslem  35941  mclspps  35942  weiunfrlem  36832  weiunpo  36833  weiunso  36834  weiunfr  36835  weiunse  36836  iblabsnclem  38189  dvasin  38210  isbnd3  38290  heiborlem3  38319  iccbnd  38346  rngohomf  38472  idlss  38522  lshplss  39612  opoccl  39825  opococ  39826  oplecon3  39830  hloml  39988  lclkrslem1  42168  lclkrslem2  42169  dvrelog2  42688  dvrelog3  42689  aks4d1p1p5  42699  primrootsunit1  42721  primrootscoprmpow  42723  primrootscoprbij  42726  primrootspoweq0  42730  aks6d1c1p2  42733  aks6d1c1p3  42734  aks6d1c1p4  42735  aks6d1c1p5  42736  aks6d1c1p7  42737  aks6d1c1p6  42738  aks6d1c1p8  42739  aks6d1c2lem3  42750  aks6d1c2lem4  42751  aks6d1c2  42754  aks6d1c6lem2  42795  aks6d1c6lem3  42796  aks6d1c6lem4  42797  aks6d1c6isolem1  42798  aks6d1c6isolem2  42799  aks6d1c6lem5  42801  aks5lem1  42810  aks5lem2  42811  aks5lem3a  42813  flt4lem5f  43246  flt4lem7  43248  nna4b4nsq  43249  eliccre  46080  eliocre  46084  icoiccdif  46099  limccog  46195  lptioo1  46207  cncfiooicclem1  46466  ditgeqiooicc  46533  stoweidlem30  46603  stoweidlem31  46604  stoweidlem38  46611  stoweidlem44  46617  fourierdlem26  46706  fourierdlem32  46712  fourierdlem33  46713  fourierdlem37  46717  fourierdlem42  46722  fourierdlem54  46733  fourierdlem63  46742  fourierdlem64  46743  fourierdlem65  46744  fourierdlem69  46748  fourierdlem79  46758  fourierdlem82  46761  fourierdlem89  46768  fourierdlem90  46769  fourierdlem91  46770  fourierdlem111  46790  0sal  46893  hoidmv1lelem3  47166  smfdmss  47306  sigardiv  47434  sigarcol  47437  sharhght  47438  sigaradd  47439  cevathlem1  47440  cevathlem2  47441  cevath  47442  nthrucw  47461  proththd  48222  perfectALTVlem2  48343  isuspgrim0  48515  gpgnbgrvtx0  48695  gpgnbgrvtx1  48696  itsclc0yqsol  49396  imaf1hom  49738