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  7202  f1dom3el3dif  7203  f1prex  7218  oeeui  8517  oeeu  8518  domssex2  9050  domssex  9051  cantnflem1a  9575  cantnflem1b  9576  cantnflem1c  9577  cantnflem1d  9578  cantnflem1  9579  cantnflem3  9581  cantnflem4  9582  fpwwe2lem6  10524  canthnumlem  10536  canthp1lem2  10541  wuntr  10593  lelttrdi  11272  supmul1  12088  supmullem1  12089  supmullem2  12090  supmul  12091  ixxdisj  13257  ixxun  13258  ixxss1  13260  ixxss2  13261  ixxss12  13262  ixxub  13263  ixxlb  13264  iccss2  13314  iocssre  13324  icossre  13325  iccssre  13326  icodisj  13373  iccf1o  13393  xov1plusxeqvd  13395  fzen  13438  intfracq  13760  fldiv  13761  remul  15033  01sqrexlem6  15151  resqrtth  15159  sqrtth  15269  ruclem6  16141  ruclem9  16144  ruclem12  16147  gcdn0cl  16410  crth  16686  phimullem  16687  eulerthlem1  16689  eulerthlem2  16690  pcpremul  16752  prmreclem3  16827  sectcan  17659  sectco  17660  sectmon  17686  monsect  17687  funcf1  17770  funcsect  17776  invfuc  17881  coapm  17975  catciso  18015  psrel  18472  pstr  18480  mhmf  18694  submss  18714  eqger  19088  eqgcpbl  19092  gaorber  19218  orbstafun  19221  cayleyth  19325  dprdgrp  19917  dprdff  19924  ablfac1a  19981  ablfac1b  19982  lmodvscl  20809  lbsss  21009  2idlcpblrng  21206  mpfind  22040  mdetunilem2  22526  mdetunilem5  22529  mdetunilem6  22530  chfacfisfcpmat  22768  cnptop1  23155  lmfpm  23208  lmff  23214  lmcnp  23217  flimtop  23878  tlmtmd  24100  ustssxp  24118  ustdiag  24122  ustfilxp  24126  ustbas2  24138  tusbas  24180  imasdsf1olem  24286  xmeter  24346  tmsbas  24396  metustexhalf  24469  nlmngp  24590  qdensere  24682  blcvx  24711  tgqioo  24713  icccmplem2  24737  reconnlem1  24740  cnmpopc  24847  icoopnst  24861  iocopnst  24862  iccpnfcnv  24867  phtpcer  24919  phtpcco2  24924  pcohtpylem  24944  pcohtpy  24945  pcopt  24947  pcopt2  24948  pcorevlem  24951  pcorev2  24953  pcophtb  24954  om1addcl  24958  pi1grplem  24974  pi1inv  24977  pi1xfrf  24978  pi1xfr  24980  pi1xfrcnvlem  24981  pi1xfrcnv  24982  pi1cof  24984  pi1coghm  24986  cphphl  25096  cphreccllem  25103  cphsqrtcl2  25111  phclm  25157  tcphcph  25162  lmcau  25238  bcthlem4  25252  minveclem4c  25350  minveclem2  25351  minveclem3b  25353  minveclem4  25357  minveclem6  25359  ivthicc  25384  ovolfsval  25396  ovollb2lem  25414  ovolshftlem1  25435  ovolscalem1  25439  ovolicc2lem2  25444  ovolicc2lem5  25447  ovolicopnf  25450  ioombl1lem1  25484  ioombl1lem3  25486  ioombl1lem4  25487  uniioovol  25505  uniioombllem2a  25508  uniioombllem2  25509  uniioombllem3a  25510  uniioombllem3  25511  uniioombllem4  25512  uniioombllem6  25514  vitalilem2  25535  vitalilem3  25536  vitalilem4  25537  i1ff  25602  itg2monolem1  25676  itgreval  25723  ibladd  25747  iblabslem  25754  itgspliticc  25763  itgsplitioo  25764  ditgcl  25784  ditgswap  25785  ditgsplitlem  25786  ditgsplit  25787  limcresi  25811  dvlip2  25925  dveq0  25930  dvcnvre  25949  dvfsumlem2  25958  dvfsumlem2OLD  25959  ftc1a  25969  ply1rem  26096  facth1  26097  fta1glem1  26098  fta1glem2  26099  ig1pcl  26109  ig1pdvds  26110  plyrem  26238  facth  26239  vieta1lem1  26243  vieta1lem2  26244  aaliou3lem3  26277  aaliou3lem7  26282  pserulm  26356  psercnlem2  26359  psercn  26361  pserdvlem1  26362  pserdvlem2  26363  pserdv  26364  abelth2  26377  coseq00topi  26436  coseq0negpitopi  26437  cosordlem  26464  efif1olem1  26476  dvloglem  26582  loglesqrt  26696  relogbval  26707  nnlogbexp  26716  logbrec  26717  quart1  26791  quartlem2  26793  quartlem3  26794  quartlem4  26795  quart  26796  asinsinlem  26826  atanlogsublem  26850  atans2  26866  dvatan  26870  rlimcnp2  26901  divsqrtsumlem  26915  ftalem5  27012  ftalem7  27014  basellem4  27019  basellem5  27020  perfectlem2  27166  dchrinv  27197  chpdifbndlem1  27489  pntibndlem2  27527  pntlema  27532  pntlemb  27533  pntlemg  27534  pntlemh  27535  pntlemn  27536  pntlemq  27537  pntlemr  27538  pntlemj  27539  pntlemf  27541  pntlemk  27542  pntlemo  27543  pntlemp  27546  pntleml  27547  abvcxp  27551  scutcl  27741  scutun12  27749  sltrec  27760  addsproplem6  27915  addsprop  27917  addscld  27921  negsproplem6  27973  negsprop  27975  mulsproplem11  28063  mulsproplem12  28064  axtgbtwnid  28442  cgr3simp1  28496  hlne1  28581  hltr  28586  btwnhl  28590  mirhl  28655  opphllem4  28726  hlpasch  28732  inagswap  28817  inagne1  28818  dfcgrg2  28839  wlkf  29591  wlk1ewlk  29616  2wlkdlem6  29907  2wlkond  29913  2trlond  29915  grpofo  30474  vcablo  30544  nvvc  30590  sspba  30702  sspg  30703  minvecolem2  30850  minvecolem4c  30854  minvecolem4  30855  minvecolem5  30856  minvecolem6  30857  eleigveccl  31934  tpssad  32514  xrofsup  32745  eliccelico  32755  elicoelioo  32756  cyc3evpm  33114  slmdvscl  33178  slmdvsass  33181  imaslmod  33313  prmidlidl  33404  mxidlidl  33423  0ringmon1p  33515  irngss  33695  algextdeglem1  33725  constrsqrtcl  33787  baselsiga  34123  insiga  34145  ldsysgenld  34168  sigapildsys  34170  ldgenpisyslem1  34171  measfrge0  34211  sibfmbl  34343  eulerpartlemt  34379  eulerpartlemmf  34383  probfinmeasbALTV  34437  tg5segofs  34681  pfxwlk  35156  revwlk  35157  subgrwlk  35164  subfacp1lem2a  35212  subfacp1lem2b  35213  subfacp1lem3  35214  subfacp1lem4  35215  subfacp1lem5  35216  sconnpht2  35270  sconnpi1  35271  cvxsconn  35275  cvmlift2lem3  35337  cvmlift2lem5  35339  cvmlift2lem6  35340  cvmlift2lem7  35341  cvmlift2lem12  35346  cvmliftphtlem  35349  cvmliftpht  35350  cvmlift3lem2  35352  cvmlift3lem4  35354  cvmlift3lem5  35355  cvmlift3lem6  35356  msrf  35574  elmsta  35580  mthmpps  35614  mclsppslem  35615  mclspps  35616  weiunfrlem  36497  weiunpo  36498  weiunso  36499  weiunfr  36500  weiunse  36501  iblabsnclem  37722  dvasin  37743  isbnd3  37823  heiborlem3  37852  iccbnd  37879  rngohomf  38005  idlss  38055  lshplss  39019  opoccl  39232  opococ  39233  oplecon3  39237  hloml  39395  lclkrslem1  41575  lclkrslem2  41576  dvrelog2  42096  dvrelog3  42097  aks4d1p1p5  42107  primrootsunit1  42129  primrootscoprmpow  42131  primrootscoprbij  42134  primrootspoweq0  42138  aks6d1c1p2  42141  aks6d1c1p3  42142  aks6d1c1p4  42143  aks6d1c1p5  42144  aks6d1c1p7  42145  aks6d1c1p6  42146  aks6d1c1p8  42147  aks6d1c2lem3  42158  aks6d1c2lem4  42159  aks6d1c2  42162  aks6d1c6lem2  42203  aks6d1c6lem3  42204  aks6d1c6lem4  42205  aks6d1c6isolem1  42206  aks6d1c6isolem2  42207  aks6d1c6lem5  42209  aks5lem1  42218  aks5lem2  42219  aks5lem3a  42221  evlsval3  42591  flt4lem5f  42689  flt4lem7  42691  nna4b4nsq  42692  eliccre  45544  eliocre  45548  icoiccdif  45563  limccog  45659  lptioo1  45671  cncfiooicclem1  45930  ditgeqiooicc  45997  stoweidlem30  46067  stoweidlem31  46068  stoweidlem38  46075  stoweidlem44  46081  fourierdlem26  46170  fourierdlem32  46176  fourierdlem33  46177  fourierdlem37  46181  fourierdlem42  46186  fourierdlem54  46197  fourierdlem63  46206  fourierdlem64  46207  fourierdlem65  46208  fourierdlem69  46212  fourierdlem79  46222  fourierdlem82  46225  fourierdlem89  46232  fourierdlem90  46233  fourierdlem91  46234  fourierdlem111  46254  0sal  46357  hoidmv1lelem3  46630  smfdmss  46770  sigardiv  46898  sigarcol  46901  sharhght  46902  sigaradd  46903  cevathlem1  46904  cevathlem2  46905  cevath  46906  proththd  47644  perfectALTVlem2  47752  isuspgrim0  47924  gpgnbgrvtx0  48104  gpgnbgrvtx1  48105  itsclc0yqsol  48795  imaf1hom  49139