Theorem simp2d 1144

Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
3simp1d.1	⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp2d	⊢ (𝜑 → 𝜒)

Proof of Theorem simp2d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp2 1138	. 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:  simp2bi  1147  f1dom3fv3dif  7288  f1dom3el3dif  7289  f1prex  7304  oeeui  8640  resixp  8973  domssex  9178  cantnflem1a  9725  cantnflem1d  9728  cantnflem3  9731  cantnflem4  9732  fpwwe2lem6  10676  canthnumlem  10688  canthp1lem2  10693  wun0  10758  lelttrdi  11423  supmullem2  12239  supmul  12240  ixxdisj  13402  ixxun  13403  ixxss1  13405  ixxss2  13406  ixxss12  13407  ixxub  13408  ixxlb  13409  ubioo  13419  elicore  13439  iccgelb  13443  iccss2  13458  icodisj  13516  xov1plusxeqvd  13538  fldiv  13900  immul  15175  sqrtge0  15296  sqrtrege0  15404  icco1  15576  ruclem2  16268  ruclem3  16269  ruclem8  16273  ruclem12  16277  gcddvds  16540  crth  16815  phimullem  16816  eulerthlem1  16818  eulerthlem2  16819  prmreclem3  16956  sectcan  17799  sectco  17800  sectmon  17826  monsect  17827  funcixp  17912  funcsect  17917  invfuc  18022  coapm  18116  catciso  18156  posasymb  18365  ipodrsima  18586  pstr2  18616  psdmrn  18618  psref  18619  mhmlin  18806  subm0cl  18824  eqger  19196  eqgcpbl  19200  gaorber  19326  orbstafun  19329  cayleyth  19433  pmtrrn2  19478  pmtrfinv  19479  dfod2  19582  sylow2blem1  19638  dprdf  20026  dprdff  20032  dprdfcl  20033  dprdsplit  20068  dpjcntz  20072  ablfac1a  20089  ablfac1b  20090  lmodvsdi  20883  lbssp  21078  2idlcpblrng  21281  mpff  22128  mpfaddcl  22129  mpfmulcl  22130  mpfind  22131  pf1rcl  22353  mpfpf1  22355  mdetunilem2  22619  mdetunilem5  22622  mdetunilem6  22623  chfacfisfcpmat  22861  pnfnei  23228  cnptop2  23251  lmcl  23305  lmcnp  23312  flimfil  23977  tlmlmod  24197  ustbasel  24215  ustincl  24216  ustinvel  24218  ustfilxp  24221  tusunif  24278  imasdsf1olem  24383  xmeter  24443  tmsds  24497  metustexhalf  24569  nlmlmod  24699  qdensere  24790  blcvx  24819  tgqioo  24821  icccmplem2  24845  reconnlem1  24848  cnmpopc  24955  phtpcer  25027  phtpcco2  25032  pcohtpylem  25052  pcohtpy  25053  pcophtb  25062  om1addcl  25066  pi1blem  25072  pi1cpbl  25077  pi1grplem  25082  pi1inv  25085  pi1xfrf  25086  pi1xfr  25088  pi1xfrcnvlem  25089  pi1cof  25092  pi1coghm  25094  cphnlm  25206  cphsqrtcl2  25220  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  ovolicc1  25551  ovolicc2lem2  25553  ovolicc2lem4  25555  ovolicc2lem5  25556  ovolicopnf  25559  ioombl1lem1  25593  ioombl1lem3  25595  ioombl1lem4  25596  uniioovol  25614  uniioombllem2a  25617  uniioombllem2  25618  uniioombllem3a  25619  uniioombllem3  25620  uniioombllem4  25621  uniioombllem6  25623  dyadmaxlem  25632  volivth  25642  vitalilem2  25644  vitalilem5  25647  i1frn  25712  itg2monolem1  25785  itgcnlem  25825  itgrevallem1  25830  itgreval  25832  itgle  25845  ibladd  25856  iblabslem  25863  itgspliticc  25872  itgsplitioo  25873  ditgcl  25893  ditgswap  25894  ditgsplitlem  25895  limcdif  25911  limcresi  25920  limccnp  25926  limccnp2  25927  limcco  25928  dvlip  26032  dvlip2  26034  dveq0  26039  dvgt0lem1  26041  dvivthlem1  26047  dvcnvrelem1  26056  dvcnvre  26058  dvfsumlem2  26067  dvfsumlem2OLD  26068  ftc1lem1  26076  ftc1a  26078  ftc1lem4  26080  ftc2ditglem  26086  itgsubstlem  26089  ply1rem  26205  fta1glem1  26207  ig1pdvds  26219  plyrem  26347  facth  26348  fta1lem  26349  vieta1lem1  26352  vieta1lem2  26353  aaliou3lem3  26386  aaliou3lem4  26388  aaliou3lem7  26391  taylfvallem1  26398  tayl0  26403  taylply2  26409  taylply2OLD  26410  radcnvle  26463  psercnlem2  26468  psercnlem1  26469  psercn  26470  pserdvlem1  26471  pserdvlem2  26472  abelth2  26486  coseq00topi  26544  coseq0negpitopi  26545  cosordlem  26572  tanord1  26579  efif1olem1  26584  loglesqrt  26804  logreclem  26805  relogbval  26815  nnlogbexp  26824  chordthmlem4  26878  quart1  26899  quartlem2  26901  quartlem3  26902  quartlem4  26903  quart  26904  acosbnd  26943  atancj  26953  atanlogsublem  26958  atantan  26966  atanbndlem  26968  dvatan  26978  atantayl  26980  rlimcnp2  27009  divsqrtsumlem  27023  ftalem5  27120  ftalem7  27122  basellem4  27127  basellem5  27128  perfectlem2  27274  dchrinv  27305  chpdifbndlem1  27597  pntibndlem2  27635  pntlemc  27639  pntlema  27640  pntlemb  27641  pntlemg  27642  pntlemh  27643  pntlemq  27645  pntlemr  27646  pntlemj  27647  pntlemi  27648  pntlemf  27649  pntlemk  27650  pntlemo  27651  pntleme  27652  pntlem3  27653  pntleml  27655  abvcxp  27659  scutun12  27855  slerec  27864  cofcut2  27956  cofcutr  27958  cofcutrtime  27961  cutmax  27968  cutmin  27969  addsproplem4  28005  addsproplem6  28007  addsuniflem  28034  addsasslem1  28036  addsasslem2  28037  negsproplem5  28064  negsproplem6  28065  negscut2  28072  negsunif  28087  mulsproplem12  28153  ssltmul1  28173  ssltmul2  28174  mulsuniflem  28175  precsexlem11  28241  axtgpasch  28475  cgr3simp2  28529  legso  28607  hlne2  28614  hlln  28615  mirhl  28687  inagswap  28849  inagne2  28851  dfcgrg2  28871  subumgredg2  29302  upgrres1  29330  nb3grprlem1  29397  wlkp  29634  wspthsswwlkn  29938  2wlkdlem6  29951  clwwisshclwwsn  30035  erclwwlkeqlen  30038  erclwwlksym  30040  erclwwlktr  30041  clwwlkn  30045  clwwlknwrd  30053  clwwlknonex2e  30129  grpoass  30522  vcsm  30581  nvf  30679  ssps  30749  minvecolem2  30894  minvecolem4c  30898  minvecolem4  30899  minvecolem5  30900  minvecolem6  30901  eigvec1  31981  eliccelico  32779  elicoelioo  32780  pmtrto1cl  33119  cyc3evpm  33170  slmdvsdi  33221  slmdvs1  33226  sdrgdvcl  33301  sdrginvcl  33302  fldgenssp  33320  imaslmod  33381  prmidlnr  33467  qsidomlem2  33481  mxidlnr  33492  0ringmon1p  33583  irngnzply1lem  33740  irngnzply1  33741  ply1annig1p  33747  minplycl  33749  ply1annprmidl  33750  minplym1p  33756  algextdeglem1  33758  algextdeglem2  33759  algextdeglem3  33760  algextdeglem4  33761  algextdeglem5  33762  cnre2csqlem  33909  lmxrge0  33951  sigaclci  34133  difelsiga  34134  insiga  34138  ldsysgenld  34161  sigapildsyslem  34162  sigapildsys  34163  ldgenpisyslem1  34164  measvnul  34207  sibfrn  34339  eulerpartlemt  34373  eulerpartlemmf  34377  tg5segofs  34688  lpadleft  34698  spthcycl  35134  subgrwlk  35137  acycgrcycl  35152  subfacp1lem2a  35185  subfacp1lem3  35187  subfacp1lem4  35188  subfacp1lem5  35189  sconnpht2  35243  sconnpi1  35244  resconn  35251  cvmsss  35272  cvmsn0  35273  cvmlift2lem3  35310  cvmlift2lem7  35314  cvmliftphtlem  35322  cvmliftpht  35323  cvmlift3lem5  35328  cvmlift3lem6  35329  msrf  35547  elmsta  35553  mclsax  35574  mthmpps  35587  mclspps  35589  ivthALT  36336  weiunpo  36466  weiunso  36467  weiunfr  36468  weiunse  36469  poimirlem17  37644  poimirlem20  37647  ibladdnc  37684  iblabsnclem  37690  ftc1cnnclem  37698  ftc1anc  37708  ftc2nc  37709  heiborlem3  37820  iccbnd  37847  rngohom1  37975  idl0cl  38025  maxidlnr  38049  lshpne  38983  opococ  39196  opexmid  39208  hlclat  39359  lclkrslem2  41540  fzne2d  41981  dvrelog2  42065  dvrelog3  42066  0nonelalab  42068  aks4d1p1p5  42076  primrootsunit1  42098  primrootscoprmpow  42100  primrootscoprbij  42103  primrootspoweq0  42107  aks6d1c2lem3  42127  aks6d1c2  42131  aks6d1c6lem5  42178  aks5lem1  42187  aks5lem2  42188  aks5lem3a  42190  aks5lem5a  42192  unitscyglem1  42196  metakunt8  42213  metakunt21  42226  metakunt22  42227  metakunt24  42229  metakunt25  42230  evlsval3  42569  flt4lem5f  42667  flt4lem7  42669  nna4b4nsq  42670  gneispacern2  44152  cvgdvgrat  44332  iccshift  45531  iccsuble  45532  icoiccdif  45537  mullimc  45631  limccog  45635  mullimcf  45638  lptioo2  45646  limcmptdm  45650  limcicciooub  45652  xlimmnfvlem1  45847  xlimpnfvlem1  45851  icccncfext  45902  cncfioobdlem  45911  ditgeqiooicc  45975  itgsubsticc  45991  iblcncfioo  45993  itgiccshift  45995  itgperiod  45996  itgsbtaddcnst  45997  stoweidlem31  46046  stoweidlem36  46051  stoweidlem38  46053  stoweidlem44  46059  stoweidlem62  46077  dirkercncflem1  46118  dirkercncflem4  46121  fourierdlem26  46148  fourierdlem32  46154  fourierdlem33  46155  fourierdlem37  46159  fourierdlem42  46164  fourierdlem54  46175  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem69  46190  fourierdlem74  46195  fourierdlem75  46196  fourierdlem79  46200  fourierdlem81  46202  fourierdlem82  46203  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem93  46214  fourierdlem101  46222  fourierdlem111  46232  saldifcl  46334  unisalgen2  46369  hoidmv1lelem3  46608  smff  46747  sigardiv  46876  sigarcol  46879  sharhght  46880  sigaradd  46881  cevathlem1  46882  cevathlem2  46883  cevath  46884  proththd  47601  perfectALTVlem2  47709  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031  fucofulem1  49005