Theorem simp1d 1143

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  simp1bi  1146  f1dom3fv3dif  7224  f1dom3el3dif  7225  f1prex  7240  oeeui  8540  oeeu  8541  domssex2  9077  domssex  9078  cantnflem1a  9606  cantnflem1b  9607  cantnflem1c  9608  cantnflem1d  9609  cantnflem1  9610  cantnflem3  9612  cantnflem4  9613  fpwwe2lem6  10559  canthnumlem  10571  canthp1lem2  10576  wuntr  10628  lelttrdi  11307  supmul1  12123  supmullem1  12124  supmullem2  12125  supmul  12126  ixxdisj  13288  ixxun  13289  ixxss1  13291  ixxss2  13292  ixxss12  13293  ixxub  13294  ixxlb  13295  iccss2  13345  iocssre  13355  icossre  13356  iccssre  13357  icodisj  13404  iccf1o  13424  xov1plusxeqvd  13426  fzen  13469  intfracq  13791  fldiv  13792  remul  15064  01sqrexlem6  15182  resqrtth  15190  sqrtth  15300  ruclem6  16172  ruclem9  16175  ruclem12  16178  gcdn0cl  16441  crth  16717  phimullem  16718  eulerthlem1  16720  eulerthlem2  16721  pcpremul  16783  prmreclem3  16858  sectcan  17691  sectco  17692  sectmon  17718  monsect  17719  funcf1  17802  funcsect  17808  invfuc  17913  coapm  18007  catciso  18047  psrel  18504  pstr  18512  mhmf  18726  submss  18746  eqger  19119  eqgcpbl  19123  gaorber  19249  orbstafun  19252  cayleyth  19356  dprdgrp  19948  dprdff  19955  ablfac1a  20012  ablfac1b  20013  lmodvscl  20841  lbsss  21041  2idlcpblrng  21238  evlsval3  22056  mpfind  22082  mdetunilem2  22569  mdetunilem5  22572  mdetunilem6  22573  chfacfisfcpmat  22811  cnptop1  23198  lmfpm  23251  lmff  23257  lmcnp  23260  flimtop  23921  tlmtmd  24143  ustssxp  24161  ustdiag  24165  ustfilxp  24169  ustbas2  24181  tusbas  24223  imasdsf1olem  24329  xmeter  24389  tmsbas  24439  metustexhalf  24512  nlmngp  24633  qdensere  24725  blcvx  24754  tgqioo  24756  icccmplem2  24780  reconnlem1  24783  cnmpopc  24890  icoopnst  24904  iocopnst  24905  iccpnfcnv  24910  phtpcer  24962  phtpcco2  24967  pcohtpylem  24987  pcohtpy  24988  pcopt  24990  pcopt2  24991  pcorevlem  24994  pcorev2  24996  pcophtb  24997  om1addcl  25001  pi1grplem  25017  pi1inv  25020  pi1xfrf  25021  pi1xfr  25023  pi1xfrcnvlem  25024  pi1xfrcnv  25025  pi1cof  25027  pi1coghm  25029  cphphl  25139  cphreccllem  25146  cphsqrtcl2  25154  phclm  25200  tcphcph  25205  lmcau  25281  bcthlem4  25295  minveclem4c  25393  minveclem2  25394  minveclem3b  25396  minveclem4  25400  minveclem6  25402  ivthicc  25427  ovolfsval  25439  ovollb2lem  25457  ovolshftlem1  25478  ovolscalem1  25482  ovolicc2lem2  25487  ovolicc2lem5  25490  ovolicopnf  25493  ioombl1lem1  25527  ioombl1lem3  25529  ioombl1lem4  25530  uniioovol  25548  uniioombllem2a  25551  uniioombllem2  25552  uniioombllem3a  25553  uniioombllem3  25554  uniioombllem4  25555  uniioombllem6  25557  vitalilem2  25578  vitalilem3  25579  vitalilem4  25580  i1ff  25645  itg2monolem1  25719  itgreval  25766  ibladd  25790  iblabslem  25797  itgspliticc  25806  itgsplitioo  25807  ditgcl  25827  ditgswap  25828  ditgsplitlem  25829  ditgsplit  25830  limcresi  25854  dvlip2  25968  dveq0  25973  dvcnvre  25992  dvfsumlem2  26001  dvfsumlem2OLD  26002  ftc1a  26012  ply1rem  26139  facth1  26140  fta1glem1  26141  fta1glem2  26142  ig1pcl  26152  ig1pdvds  26153  plyrem  26281  facth  26282  vieta1lem1  26286  vieta1lem2  26287  aaliou3lem3  26320  aaliou3lem7  26325  pserulm  26399  psercnlem2  26402  psercn  26404  pserdvlem1  26405  pserdvlem2  26406  pserdv  26407  abelth2  26420  coseq00topi  26479  coseq0negpitopi  26480  cosordlem  26507  efif1olem1  26519  dvloglem  26625  loglesqrt  26739  relogbval  26750  nnlogbexp  26759  logbrec  26760  quart1  26834  quartlem2  26836  quartlem3  26837  quartlem4  26838  quart  26839  asinsinlem  26869  atanlogsublem  26893  atans2  26909  dvatan  26913  rlimcnp2  26944  divsqrtsumlem  26958  ftalem5  27055  ftalem7  27057  basellem4  27062  basellem5  27063  perfectlem2  27209  dchrinv  27240  chpdifbndlem1  27532  pntibndlem2  27570  pntlema  27575  pntlemb  27576  pntlemg  27577  pntlemh  27578  pntlemn  27579  pntlemq  27580  pntlemr  27581  pntlemj  27582  pntlemf  27584  pntlemk  27585  pntlemo  27586  pntlemp  27589  pntleml  27590  abvcxp  27594  cutscl  27790  cutsun12  27798  ltsrec  27809  addsproplem6  27982  addsprop  27984  addscld  27988  negsproplem6  28041  negsprop  28043  mulsproplem11  28134  mulsproplem12  28135  axtgbtwnid  28550  cgr3simp1  28604  hlne1  28689  hltr  28694  btwnhl  28698  mirhl  28763  opphllem4  28834  hlpasch  28840  inagswap  28925  inagne1  28926  dfcgrg2  28947  wlkf  29700  wlk1ewlk  29725  2wlkdlem6  30016  2wlkond  30022  2trlond  30024  grpofo  30586  vcablo  30656  nvvc  30702  sspba  30814  sspg  30815  minvecolem2  30962  minvecolem4c  30966  minvecolem4  30967  minvecolem5  30968  minvecolem6  30969  eleigveccl  32046  tpssad  32625  xrofsup  32857  eliccelico  32867  elicoelioo  32868  cyc3evpm  33243  slmdvscl  33307  slmdvsass  33310  imaslmod  33445  prmidlidl  33536  mxidlidl  33555  0ringmon1p  33649  irngss  33864  algextdeglem1  33894  constrsqrtcl  33956  baselsiga  34292  insiga  34314  ldsysgenld  34337  sigapildsys  34339  ldgenpisyslem1  34340  measfrge0  34380  sibfmbl  34512  eulerpartlemt  34548  eulerpartlemmf  34552  probfinmeasbALTV  34606  tg5segofs  34850  pfxwlk  35337  revwlk  35338  subgrwlk  35345  subfacp1lem2a  35393  subfacp1lem2b  35394  subfacp1lem3  35395  subfacp1lem4  35396  subfacp1lem5  35397  sconnpht2  35451  sconnpi1  35452  cvxsconn  35456  cvmlift2lem3  35518  cvmlift2lem5  35520  cvmlift2lem6  35521  cvmlift2lem7  35522  cvmlift2lem12  35527  cvmliftphtlem  35530  cvmliftpht  35531  cvmlift3lem2  35533  cvmlift3lem4  35535  cvmlift3lem5  35536  cvmlift3lem6  35537  msrf  35755  elmsta  35761  mthmpps  35795  mclsppslem  35796  mclspps  35797  weiunfrlem  36677  weiunpo  36678  weiunso  36679  weiunfr  36680  weiunse  36681  iblabsnclem  37931  dvasin  37952  isbnd3  38032  heiborlem3  38061  iccbnd  38088  rngohomf  38214  idlss  38264  lshplss  39354  opoccl  39567  opococ  39568  oplecon3  39572  hloml  39730  lclkrslem1  41910  lclkrslem2  41911  dvrelog2  42431  dvrelog3  42432  aks4d1p1p5  42442  primrootsunit1  42464  primrootscoprmpow  42466  primrootscoprbij  42469  primrootspoweq0  42473  aks6d1c1p2  42476  aks6d1c1p3  42477  aks6d1c1p4  42478  aks6d1c1p5  42479  aks6d1c1p7  42480  aks6d1c1p6  42481  aks6d1c1p8  42482  aks6d1c2lem3  42493  aks6d1c2lem4  42494  aks6d1c2  42497  aks6d1c6lem2  42538  aks6d1c6lem3  42539  aks6d1c6lem4  42540  aks6d1c6isolem1  42541  aks6d1c6isolem2  42542  aks6d1c6lem5  42544  aks5lem1  42553  aks5lem2  42554  aks5lem3a  42556  flt4lem5f  43012  flt4lem7  43014  nna4b4nsq  43015  eliccre  45862  eliocre  45866  icoiccdif  45881  limccog  45977  lptioo1  45989  cncfiooicclem1  46248  ditgeqiooicc  46315  stoweidlem30  46385  stoweidlem31  46386  stoweidlem38  46393  stoweidlem44  46399  fourierdlem26  46488  fourierdlem32  46494  fourierdlem33  46495  fourierdlem37  46499  fourierdlem42  46504  fourierdlem54  46515  fourierdlem63  46524  fourierdlem64  46525  fourierdlem65  46526  fourierdlem69  46530  fourierdlem79  46540  fourierdlem82  46543  fourierdlem89  46550  fourierdlem90  46551  fourierdlem91  46552  fourierdlem111  46572  0sal  46675  hoidmv1lelem3  46948  smfdmss  47088  sigardiv  47216  sigarcol  47219  sharhght  47220  sigaradd  47221  cevathlem1  47222  cevathlem2  47223  cevath  47224  nthrucw  47241  proththd  47971  perfectALTVlem2  48079  isuspgrim0  48251  gpgnbgrvtx0  48431  gpgnbgrvtx1  48432  itsclc0yqsol  49121  imaf1hom  49464