Theorem simp1d 1160

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp1bi  1163  f1dom3fv3dif  7273  f1dom3el3dif  7274  f1prex  7293  oeeui  8597  oeeu  8598  domssex2  9135  domssex  9136  cantnflem1a  9664  cantnflem1b  9665  cantnflem1c  9666  cantnflem1d  9667  cantnflem1  9668  cantnflem3  9670  cantnflem4  9671  fpwwe2lem6  10639  canthnumlem  10651  canthp1lem2  10656  wuntr  10708  lelttrdi  11390  supmul1  12202  supmullem1  12203  supmullem2  12204  supmul  12205  ixxdisj  13405  ixxun  13406  ixxss1  13408  ixxss2  13409  ixxss12  13410  ixxub  13411  ixxlb  13412  iccss2  13462  iocssre  13472  icossre  13473  iccssre  13474  icodisj  13521  iccf1o  13541  xov1plusxeqvd  13543  fzen  13587  intfracq  13912  fldiv  13913  remul  15206  01sqrexlem6  15324  resqrtth  15332  sqrtth  15442  ruclem6  16316  ruclem9  16319  ruclem12  16322  gcdn0cl  16585  crth  16862  phimullem  16863  eulerthlem1  16865  eulerthlem2  16866  pcpremul  16928  prmreclem3  17003  sectcan  17837  sectco  17838  sectmon  17864  monsect  17865  funcf1  17948  funcsect  17954  invfuc  18059  coapm  18153  catciso  18193  psrel  18650  pstr  18658  mhmf  18878  submss  18898  eqger  19277  eqgcpbl  19281  gaorber  19409  orbstafun  19412  cayleyth  19516  dprdgrp  20108  dprdff  20115  ablfac1a  20172  ablfac1b  20173  lmodvscl  21036  lbsss  21235  2idlcpblrng  21447  prmidlidl  21506  evlsval3  22277  mpfind  22303  mdetunilem2  22807  mdetunilem5  22810  mdetunilem6  22811  chfacfisfcpmat  23049  cnptop1  23436  lmfpm  23489  lmff  23495  lmcnp  23498  flimtop  24159  tlmtmd  24381  ustssxp  24399  ustdiag  24403  ustfilxp  24407  ustbas2  24419  tusbas  24461  imasdsf1olem  24567  xmeter  24627  tmsbas  24677  metustexhalf  24750  nlmngp  24871  qdensere  24963  blcvx  24992  tgqioo  24994  icccmplem2  25018  reconnlem1  25021  cnmpopc  25124  icoopnst  25135  iocopnst  25136  iccpnfcnv  25140  phtpcer  25191  phtpcco2  25195  pcohtpylem  25215  pcohtpy  25216  pcopt  25218  pcopt2  25219  pcorevlem  25222  pcorev2  25224  pcophtb  25225  om1addcl  25229  pi1grplem  25245  pi1inv  25248  pi1xfrf  25249  pi1xfr  25251  pi1xfrcnvlem  25252  pi1xfrcnv  25253  pi1cof  25255  pi1coghm  25257  cphphl  25367  cphreccllem  25374  cphsqrtcl2  25382  phclm  25428  tcphcph  25433  lmcau  25509  bcthlem4  25523  minveclem4c  25621  minveclem2  25622  minveclem3b  25624  minveclem4  25628  minveclem6  25630  ivthicc  25654  ovolfsval  25666  ovollb2lem  25684  ovolshftlem1  25705  ovolscalem1  25709  ovolicc2lem2  25714  ovolicc2lem5  25717  ovolicopnf  25720  ioombl1lem1  25754  ioombl1lem3  25756  ioombl1lem4  25757  uniioovol  25775  uniioombllem2a  25778  uniioombllem2  25779  uniioombllem3a  25780  uniioombllem3  25781  uniioombllem4  25782  uniioombllem6  25784  vitalilem2  25805  vitalilem3  25806  vitalilem4  25807  i1ff  25872  itg2monolem1  25946  itgreval  25993  ibladd  26017  iblabslem  26024  itgspliticc  26033  itgsplitioo  26034  ditgcl  26054  ditgswap  26055  ditgsplitlem  26056  ditgsplit  26057  limcresi  26081  dvlip2  26191  dveq0  26196  dvcnvre  26215  dvfsumlem2  26223  ftc1a  26233  ply1rem  26360  facth1  26361  fta1glem1  26362  fta1glem2  26363  ig1pcl  26373  ig1pdvds  26374  plyrem  26503  facth  26504  vieta1lem1  26508  vieta1lem2  26509  aaliou3lem3  26544  aaliou3lem7  26549  pserulm  26622  psercnlem2  26624  psercn  26626  pserdvlem1  26627  pserdvlem2  26628  pserdv  26629  abelth2  26642  coseq00topi  26704  coseq0negpitopi  26705  cosordlem  26732  efif1olem1  26744  dvloglem  26850  loglesqrt  26963  relogbval  26974  nnlogbexp  26983  logbrec  26984  quart1  27058  quartlem2  27060  quartlem3  27061  quartlem4  27062  quart  27063  asinsinlem  27093  atanlogsublem  27117  atans2  27133  dvatan  27137  rlimcnp2  27168  divsqrtsumlem  27181  ftalem5  27278  ftalem7  27280  basellem4  27285  basellem5  27286  perfectlem2  27431  dchrinv  27462  chpdifbndlem1  27754  pntibndlem2  27792  pntlema  27797  pntlemb  27798  pntlemg  27799  pntlemh  27800  pntlemn  27801  pntlemq  27802  pntlemr  27803  pntlemj  27804  pntlemf  27806  pntlemk  27807  pntlemo  27808  pntlemp  27811  pntleml  27812  abvcxp  27816  cutscl  28012  cutsun12  28020  ltsrec  28031  addsproplem6  28204  addsprop  28206  addscld  28210  negsproplem6  28263  negsprop  28265  mulsproplem11  28356  mulsproplem12  28357  axtgbtwnid  28772  cgr3simp1  28826  hlne1  28914  hltr  28919  btwnhl  28923  mirhl  28993  opphllem4  29068  hlpasch  29075  inagswap  29195  inagne1  29196  dfcgrg2  29217  wlkf  30001  wlk1ewlk  30026  2wlkdlem6  30317  2wlkond  30323  2trlond  30325  grpofo  30888  vcablo  30958  nvvc  31004  sspba  31116  sspg  31117  minvecolem2  31264  minvecolem4c  31268  minvecolem4  31269  minvecolem5  31270  minvecolem6  31271  eleigveccl  32348  tpssad  32922  xrofsup  33149  eliccelico  33159  elicoelioo  33160  cyc3evpm  33501  slmdvscl  33565  slmdvsass  33568  imaslmod  33704  mxidlidl  33777  0ringmon1p  33878  irngss  34108  algextdeglem1  34138  constrsqrtcl  34200  baselsiga  34536  insiga  34559  ldsysgenld  34582  sigapildsys  34584  ldgenpisyslem1  34585  measfrge0  34625  sibfmbl  34757  eulerpartlemt  34793  eulerpartlemmf  34797  probfinmeasbALTV  34851  tg5segofs  35095  pfxwlk  35637  revwlk  35638  subgrwlk  35645  subfacp1lem2a  35693  subfacp1lem2b  35694  subfacp1lem3  35695  subfacp1lem4  35696  subfacp1lem5  35697  sconnpht2  35751  sconnpi1  35752  cvxsconn  35756  cvmlift2lem3  35818  cvmlift2lem5  35820  cvmlift2lem6  35821  cvmlift2lem7  35822  cvmlift2lem12  35827  cvmliftphtlem  35830  cvmliftpht  35831  cvmlift3lem2  35833  cvmlift3lem4  35835  cvmlift3lem5  35836  cvmlift3lem6  35837  msrf  36055  elmsta  36061  mthmpps  36095  mclsppslem  36096  mclspps  36097  weiunfrlem  37016  weiunpo  37017  weiunso  37018  weiunfr  37019  weiunse  37020  iblabsnclem  38375  dvasin  38396  isbnd3  38476  heiborlem3  38505  iccbnd  38532  rngohomf  38658  idlss  38708  lshplss  39796  opoccl  40009  opococ  40010  oplecon3  40014  hloml  40172  lclkrslem1  42352  lclkrslem2  42353  dvrelog2  42872  dvrelog3  42873  aks4d1p1p5  42883  primrootsunit1  42905  primrootscoprmpow  42907  primrootscoprbij  42910  primrootspoweq0  42914  aks6d1c1p2  42917  aks6d1c1p3  42918  aks6d1c1p4  42919  aks6d1c1p5  42920  aks6d1c1p7  42921  aks6d1c1p6  42922  aks6d1c1p8  42923  aks6d1c2lem3  42934  aks6d1c2lem4  42935  aks6d1c2  42938  aks6d1c6lem2  42979  aks6d1c6lem3  42980  aks6d1c6lem4  42981  aks6d1c6isolem1  42982  aks6d1c6isolem2  42983  aks6d1c6lem5  42985  aks5lem1  42994  aks5lem2  42995  aks5lem3a  42997  flt4lem5f  43430  flt4lem7  43432  nna4b4nsq  43433  eliccre  46262  eliocre  46266  icoiccdif  46281  limccog  46377  lptioo1  46389  cncfiooicclem1  46648  ditgeqiooicc  46715  stoweidlem30  46785  stoweidlem31  46786  stoweidlem38  46793  stoweidlem44  46799  fourierdlem26  46888  fourierdlem32  46894  fourierdlem33  46895  fourierdlem37  46899  fourierdlem42  46904  fourierdlem54  46915  fourierdlem63  46924  fourierdlem64  46925  fourierdlem65  46926  fourierdlem69  46930  fourierdlem79  46940  fourierdlem82  46943  fourierdlem89  46950  fourierdlem90  46951  fourierdlem91  46952  fourierdlem111  46972  0sal  47075  hoidmv1lelem3  47348  smfdmss  47488  sigardiv  47616  sigarcol  47619  sharhght  47620  sigaradd  47621  cevathlem1  47622  cevathlem2  47623  cevath  47624  proththd  48407  perfectALTVlem2  48528  isuspgrim0  48700  gpgnbgrvtx0  48880  gpgnbgrvtx1  48881  itsclc0yqsol  49585  imaf1hom  49927