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  7288  f1dom3el3dif  7289  f1prex  7304  oeeui  8640  oeeu  8641  domssex2  9177  domssex  9178  cantnflem1a  9725  cantnflem1b  9726  cantnflem1c  9727  cantnflem1d  9728  cantnflem1  9729  cantnflem3  9731  cantnflem4  9732  fpwwe2lem6  10676  canthnumlem  10688  canthp1lem2  10693  wuntr  10745  lelttrdi  11423  supmul1  12237  supmullem1  12238  supmullem2  12239  supmul  12240  ixxdisj  13402  ixxun  13403  ixxss1  13405  ixxss2  13406  ixxss12  13407  ixxub  13408  ixxlb  13409  iccss2  13458  iocssre  13467  icossre  13468  iccssre  13469  icodisj  13516  iccf1o  13536  xov1plusxeqvd  13538  fzen  13581  intfracq  13899  fldiv  13900  remul  15168  01sqrexlem6  15286  resqrtth  15294  sqrtth  15403  ruclem6  16271  ruclem9  16274  ruclem12  16277  gcdn0cl  16539  crth  16815  phimullem  16816  eulerthlem1  16818  eulerthlem2  16819  pcpremul  16881  prmreclem3  16956  sectcan  17799  sectco  17800  sectmon  17826  monsect  17827  funcf1  17911  funcsect  17917  invfuc  18022  coapm  18116  catciso  18156  psrel  18614  pstr  18622  mhmf  18802  submss  18822  eqger  19196  eqgcpbl  19200  gaorber  19326  orbstafun  19329  cayleyth  19433  dprdgrp  20025  dprdff  20032  ablfac1a  20089  ablfac1b  20090  lmodvscl  20876  lbsss  21076  2idlcpblrng  21281  mpfind  22131  mdetunilem2  22619  mdetunilem5  22622  mdetunilem6  22623  chfacfisfcpmat  22861  cnptop1  23250  lmfpm  23303  lmff  23309  lmcnp  23312  flimtop  23973  tlmtmd  24195  ustssxp  24213  ustdiag  24217  ustfilxp  24221  ustbas2  24234  tusbas  24277  imasdsf1olem  24383  xmeter  24443  tmsbas  24496  metustexhalf  24569  nlmngp  24698  qdensere  24790  blcvx  24819  tgqioo  24821  icccmplem2  24845  reconnlem1  24848  cnmpopc  24955  icoopnst  24969  iocopnst  24970  iccpnfcnv  24975  phtpcer  25027  phtpcco2  25032  pcohtpylem  25052  pcohtpy  25053  pcopt  25055  pcopt2  25056  pcorevlem  25059  pcorev2  25061  pcophtb  25062  om1addcl  25066  pi1grplem  25082  pi1inv  25085  pi1xfrf  25086  pi1xfr  25088  pi1xfrcnvlem  25089  pi1xfrcnv  25090  pi1cof  25092  pi1coghm  25094  cphphl  25205  cphreccllem  25212  cphsqrtcl2  25220  phclm  25266  tcphcph  25271  lmcau  25347  bcthlem4  25361  minveclem4c  25459  minveclem2  25460  minveclem3b  25462  minveclem4  25466  minveclem6  25468  ivthicc  25493  ovolfsval  25505  ovollb2lem  25523  ovolshftlem1  25544  ovolscalem1  25548  ovolicc2lem2  25553  ovolicc2lem5  25556  ovolicopnf  25559  ioombl1lem1  25593  ioombl1lem3  25595  ioombl1lem4  25596  uniioovol  25614  uniioombllem2a  25617  uniioombllem2  25618  uniioombllem3a  25619  uniioombllem3  25620  uniioombllem4  25621  uniioombllem6  25623  vitalilem2  25644  vitalilem3  25645  vitalilem4  25646  i1ff  25711  itg2monolem1  25785  itgreval  25832  ibladd  25856  iblabslem  25863  itgspliticc  25872  itgsplitioo  25873  ditgcl  25893  ditgswap  25894  ditgsplitlem  25895  ditgsplit  25896  limcresi  25920  dvlip2  26034  dveq0  26039  dvcnvre  26058  dvfsumlem2  26067  dvfsumlem2OLD  26068  ftc1a  26078  ply1rem  26205  facth1  26206  fta1glem1  26207  fta1glem2  26208  ig1pcl  26218  ig1pdvds  26219  plyrem  26347  facth  26348  vieta1lem1  26352  vieta1lem2  26353  aaliou3lem3  26386  aaliou3lem7  26391  pserulm  26465  psercnlem2  26468  psercn  26470  pserdvlem1  26471  pserdvlem2  26472  pserdv  26473  abelth2  26486  coseq00topi  26544  coseq0negpitopi  26545  cosordlem  26572  efif1olem1  26584  dvloglem  26690  loglesqrt  26804  relogbval  26815  nnlogbexp  26824  logbrec  26825  quart1  26899  quartlem2  26901  quartlem3  26902  quartlem4  26903  quart  26904  asinsinlem  26934  atanlogsublem  26958  atans2  26974  dvatan  26978  rlimcnp2  27009  divsqrtsumlem  27023  ftalem5  27120  ftalem7  27122  basellem4  27127  basellem5  27128  perfectlem2  27274  dchrinv  27305  chpdifbndlem1  27597  pntibndlem2  27635  pntlema  27640  pntlemb  27641  pntlemg  27642  pntlemh  27643  pntlemn  27644  pntlemq  27645  pntlemr  27646  pntlemj  27647  pntlemf  27649  pntlemk  27650  pntlemo  27651  pntlemp  27654  pntleml  27655  abvcxp  27659  scutcl  27847  scutun12  27855  sltrec  27865  addsproplem6  28007  addsprop  28009  addscld  28013  negsproplem6  28065  negsprop  28067  mulsproplem11  28152  mulsproplem12  28153  axtgbtwnid  28474  cgr3simp1  28528  hlne1  28613  hltr  28618  btwnhl  28622  mirhl  28687  opphllem4  28758  hlpasch  28764  inagswap  28849  inagne1  28850  dfcgrg2  28871  wlkf  29632  wlk1ewlk  29658  2wlkdlem6  29951  2wlkond  29957  2trlond  29959  grpofo  30518  vcablo  30588  nvvc  30634  sspba  30746  sspg  30747  minvecolem2  30894  minvecolem4c  30898  minvecolem4  30899  minvecolem5  30900  minvecolem6  30901  eleigveccl  31978  xrofsup  32771  eliccelico  32779  elicoelioo  32780  cyc3evpm  33170  slmdvscl  33220  slmdvsass  33223  imaslmod  33381  prmidlidl  33472  mxidlidl  33491  0ringmon1p  33583  irngss  33737  algextdeglem1  33758  baselsiga  34116  insiga  34138  ldsysgenld  34161  sigapildsys  34163  ldgenpisyslem1  34164  measfrge0  34204  sibfmbl  34337  eulerpartlemt  34373  eulerpartlemmf  34377  probfinmeasbALTV  34431  tg5segofs  34688  pfxwlk  35129  revwlk  35130  subgrwlk  35137  subfacp1lem2a  35185  subfacp1lem2b  35186  subfacp1lem3  35187  subfacp1lem4  35188  subfacp1lem5  35189  sconnpht2  35243  sconnpi1  35244  cvxsconn  35248  cvmlift2lem3  35310  cvmlift2lem5  35312  cvmlift2lem6  35313  cvmlift2lem7  35314  cvmlift2lem12  35319  cvmliftphtlem  35322  cvmliftpht  35323  cvmlift3lem2  35325  cvmlift3lem4  35327  cvmlift3lem5  35328  cvmlift3lem6  35329  msrf  35547  elmsta  35553  mthmpps  35587  mclsppslem  35588  mclspps  35589  weiunfrlem  36465  weiunpo  36466  weiunso  36467  weiunfr  36468  weiunse  36469  iblabsnclem  37690  dvasin  37711  isbnd3  37791  heiborlem3  37820  iccbnd  37847  rngohomf  37973  idlss  38023  lshplss  38982  opoccl  39195  opococ  39196  oplecon3  39200  hloml  39358  lclkrslem1  41539  lclkrslem2  41540  dvrelog2  42065  dvrelog3  42066  aks4d1p1p5  42076  primrootsunit1  42098  primrootscoprmpow  42100  primrootscoprbij  42103  primrootspoweq0  42107  aks6d1c1p2  42110  aks6d1c1p3  42111  aks6d1c1p4  42112  aks6d1c1p5  42113  aks6d1c1p7  42114  aks6d1c1p6  42115  aks6d1c1p8  42116  aks6d1c2lem3  42127  aks6d1c2lem4  42128  aks6d1c2  42131  aks6d1c6lem2  42172  aks6d1c6lem3  42173  aks6d1c6lem4  42174  aks6d1c6isolem1  42175  aks6d1c6isolem2  42176  aks6d1c6lem5  42178  aks5lem1  42187  aks5lem2  42188  aks5lem3a  42190  metakunt8  42213  metakunt19  42224  metakunt21  42226  metakunt22  42227  metakunt25  42230  evlsval3  42569  flt4lem5f  42667  flt4lem7  42669  nna4b4nsq  42670  eliccre  45518  eliocre  45522  icoiccdif  45537  limccog  45635  lptioo1  45647  cncfiooicclem1  45908  ditgeqiooicc  45975  stoweidlem30  46045  stoweidlem31  46046  stoweidlem38  46053  stoweidlem44  46059  fourierdlem26  46148  fourierdlem32  46154  fourierdlem33  46155  fourierdlem37  46159  fourierdlem42  46164  fourierdlem54  46175  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem69  46190  fourierdlem79  46200  fourierdlem82  46203  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem111  46232  0sal  46335  hoidmv1lelem3  46608  smfdmss  46748  sigardiv  46876  sigarcol  46879  sharhght  46880  sigaradd  46881  cevathlem1  46882  cevathlem2  46883  cevath  46884  proththd  47601  perfectALTVlem2  47709  isuspgrim0  47872  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031  itsclc0yqsol  48685