Theorem simp1d 1165

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

Syntax hints:   → wi 4   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  simp1bi  1168  f1dom3fv3dif  6746  f1dom3el3dif  6747  f1prex  6760  oeeui  7916  oeeu  7917  domssex2  8356  domssex  8357  cantnflem1a  8826  cantnflem1b  8827  cantnflem1c  8828  cantnflem1d  8829  cantnflem1  8830  cantnflem3  8832  cantnflem4  8833  fpwwe2lem7  9740  canthnumlem  9752  canthp1lem2  9757  wuntr  9809  lelttrdi  10481  supmul1  11274  supmullem1  11275  supmullem2  11276  supmul  11277  ixxdisj  12404  ixxun  12405  ixxss1  12407  ixxss2  12408  ixxss12  12409  ixxub  12410  ixxlb  12411  iccss2  12458  iocssre  12467  icossre  12468  iccssre  12469  icodisj  12514  iccf1o  12535  xov1plusxeqvd  12537  fzen  12577  intfracq  12878  fldiv  12879  remul  14088  sqrlem6  14207  resqrtth  14215  sqrtth  14323  ruclem6  15180  ruclem9  15183  ruclem12  15186  gcdn0cl  15439  crth  15696  phimullem  15697  eulerthlem1  15699  eulerthlem2  15700  pcpremul  15761  prmreclem3  15835  sectcan  16615  sectco  16616  sectmon  16642  monsect  16643  funcf1  16726  funcsect  16732  invfuc  16834  coapm  16921  catciso  16957  psrel  17404  pstr  17412  mhmf  17541  submss  17551  eqger  17842  eqgcpbl  17846  gaorber  17938  orbstafun  17941  cayleyth  18032  dprdgrp  18602  dprdff  18609  ablfac1a  18666  ablfac1b  18667  lmodvscl  19080  lbsss  19280  2idlcpbl  19439  assalmod  19524  mpfind  19740  mdetunilem2  20626  mdetunilem5  20629  mdetunilem6  20630  chfacfisfcpmat  20869  cnptop1  21256  lmfpm  21309  lmff  21315  lmcnp  21318  flimtop  21978  tlmtmd  22199  ustssxp  22217  ustdiag  22221  ustfilxp  22225  ustbas2  22238  tusbas  22281  imasdsf1olem  22387  xmeter  22447  tmsbas  22497  metustexhalf  22570  nlmngp  22690  qdensere  22782  blcvx  22810  tgqioo  22812  icccmplem2  22835  reconnlem1  22838  cnmpt2pc  22936  icoopnst  22947  iocopnst  22948  iccpnfcnv  22952  phtpcer  23003  phtpcco2  23007  pcohtpylem  23027  pcohtpy  23028  pcopt  23030  pcopt2  23031  pcorevlem  23034  pcorev2  23036  pcophtb  23037  om1addcl  23041  pi1grplem  23057  pi1inv  23060  pi1xfrf  23061  pi1xfr  23063  pi1xfrcnvlem  23064  pi1xfrcnv  23065  pi1cof  23067  pi1coghm  23069  cphphl  23179  cphreccllem  23186  cphsqrtcl2  23194  tchclm  23239  tchcph  23244  lmcau  23319  bcthlem4  23332  minveclem4c  23404  minveclem2  23405  minveclem3b  23407  minveclem4  23411  minveclem6  23413  ivthicc  23435  ovolfsval  23447  ovollb2lem  23465  ovolshftlem1  23486  ovolscalem1  23490  ovolicc2lem2  23495  ovolicc2lem5  23498  ovolicopnf  23501  ioombl1lem1  23535  ioombl1lem3  23537  ioombl1lem4  23538  uniioovol  23556  uniioombllem2a  23559  uniioombllem2  23560  uniioombllem3a  23561  uniioombllem3  23562  uniioombllem4  23563  uniioombllem6  23565  vitalilem2  23586  vitalilem3  23587  vitalilem4  23588  i1ff  23653  itg2monolem1  23727  itgreval  23773  ibladd  23797  iblabslem  23804  itgspliticc  23813  itgsplitioo  23814  ditgcl  23832  ditgswap  23833  ditgsplitlem  23834  ditgsplit  23835  limcresi  23859  dvlip2  23968  dveq0  23973  dvcnvre  23992  dvfsumlem2  24000  ftc1a  24010  ply1rem  24133  facth1  24134  fta1glem1  24135  fta1glem2  24136  ig1pcl  24145  ig1pdvds  24146  plyrem  24270  facth  24271  vieta1lem1  24275  vieta1lem2  24276  aaliou3lem3  24309  aaliou3lem7  24314  pserulm  24386  psercnlem2  24388  psercn  24390  pserdvlem1  24391  pserdvlem2  24392  pserdv  24393  abelth2  24406  coseq00topi  24465  coseq0negpitopi  24466  cosordlem  24488  efif1olem1  24499  dvloglem  24604  loglesqrt  24709  relogbval  24720  nnlogbexp  24729  logbrec  24730  quart1  24793  quartlem2  24795  quartlem3  24796  quartlem4  24797  quart  24798  asinsinlem  24828  atanlogsublem  24852  atans2  24868  dvatan  24872  rlimcnp2  24903  divsqrtsumlem  24916  ftalem5  25013  ftalem7  25015  basellem4  25020  basellem5  25021  perfectlem2  25165  dchrinv  25196  chpdifbndlem1  25452  pntibndlem2  25490  pntlema  25495  pntlemb  25496  pntlemg  25497  pntlemh  25498  pntlemn  25499  pntlemq  25500  pntlemr  25501  pntlemj  25502  pntlemf  25504  pntlemk  25505  pntlemo  25506  pntlemp  25509  pntleml  25510  abvcxp  25514  axtgbtwnid  25575  cgr3simp1  25625  hlne1  25710  hltr  25715  btwnhl  25719  mirhl  25784  opphllem4  25852  hlpasch  25858  inagswap  25940  wlkf  26734  wlk1ewlk  26760  2wlkdlem6  27067  2wlkond  27073  2trlond  27075  grpofo  27678  vcablo  27749  nvvc  27795  sspba  27907  sspg  27908  minvecolem2  28056  minvecolem4c  28060  minvecolem4  28061  minvecolem5  28062  minvecolem6  28063  eleigveccl  29143  xrofsup  29857  eliccelico  29863  elicoelioo  29864  slmdvscl  30089  slmdvsass  30092  baselsiga  30500  insiga  30522  ldsysgenld  30545  sigapildsys  30547  ldgenpisyslem1  30548  measfrge0  30588  sibfmbl  30719  eulerpartlemt  30755  eulerpartlemmf  30759  probfinmeasbOLD  30812  tg5segofs  31073  subfacp1lem2a  31482  subfacp1lem2b  31483  subfacp1lem3  31484  subfacp1lem4  31485  subfacp1lem5  31486  sconnpht2  31540  sconnpi1  31541  cvxsconn  31545  cvmlift2lem3  31607  cvmlift2lem5  31609  cvmlift2lem6  31610  cvmlift2lem7  31611  cvmlift2lem12  31616  cvmliftphtlem  31619  cvmliftpht  31620  cvmlift3lem2  31622  cvmlift3lem4  31624  cvmlift3lem5  31625  cvmlift3lem6  31626  msrf  31759  elmsta  31765  mthmpps  31799  mclsppslem  31800  mclspps  31801  scutun12  32235  scutf  32237  slerec  32241  sltrec  32242  madeval2  32254  iblabsnclem  33782  dvasin  33805  isbnd3  33891  heiborlem3  33920  iccbnd  33947  rngohomf  34073  idlss  34123  lshplss  34758  opoccl  34971  opococ  34972  oplecon3  34976  hloml  35134  lclkrslem1  37315  lclkrslem2  37316  eliccre  40209  eliocre  40213  icoiccdif  40228  limccog  40329  lptioo1  40341  cncfiooicclem1  40583  ditgeqiooicc  40652  stoweidlem30  40723  stoweidlem31  40724  stoweidlem38  40731  stoweidlem44  40737  fourierdlem26  40826  fourierdlem32  40832  fourierdlem33  40833  fourierdlem37  40837  fourierdlem42  40842  fourierdlem54  40853  fourierdlem63  40862  fourierdlem64  40863  fourierdlem65  40864  fourierdlem69  40868  fourierdlem79  40878  fourierdlem82  40881  fourierdlem89  40888  fourierdlem90  40889  fourierdlem91  40890  fourierdlem111  40910  0sal  41016  hoidmv1lelem3  41286  smfdmss  41421  smfpimltxr  41435  sigardiv  41529  sigarcol  41532  sharhght  41533  sigaradd  41534  cevathlem1  41535  cevathlem2  41536  cevath  41537  proththd  42103  perfectALTVlem2  42203