Theorem simp2d 1161

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp2bi  1164  f1dom3fv3dif  7264  f1dom3el3dif  7265  f1prex  7284  oeeui  8595  resixp  8945  domssex  9141  cantnflem1a  9670  cantnflem1d  9673  cantnflem3  9676  cantnflem4  9677  fpwwe2lem6  10699  canthnumlem  10711  canthp1lem2  10716  wun0  10781  lelttrdi  11450  supmullem2  12266  supmul  12267  ixxdisj  13469  ixxun  13470  ixxss1  13472  ixxss2  13473  ixxss12  13474  ixxub  13475  ixxlb  13476  ubioo  13486  elicore  13507  iccgelb  13511  iccss2  13526  icodisj  13585  xov1plusxeqvd  13607  fldiv  13977  immul  15280  sqrtge0  15401  sqrtrege0  15510  icco1  15684  ruclem2  16377  ruclem3  16378  ruclem8  16382  ruclem12  16386  gcddvds  16650  crth  16932  phimullem  16933  eulerthlem1  16935  eulerthlem2  16936  prmreclem3  17073  sectcan  17907  sectco  17908  sectmon  17934  monsect  17935  funcixp  18019  funcsect  18024  invfuc  18129  coapm  18223  catciso  18263  posasymb  18470  ipodrsima  18692  pstr2  18722  psdmrn  18724  psref  18725  mhmlin  18965  subm0cl  18983  eqger  19367  eqgcpbl  19371  gaorber  19499  orbstafun  19502  cayleyth  19606  pmtrrn2  19651  pmtrfinv  19652  dfod2  19755  sylow2blem1  19811  dprdf  20199  dprdff  20205  dprdfcl  20206  dprdsplit  20241  dpjcntz  20245  ablfac1a  20262  ablfac1b  20263  lmodvsdi  21137  lbssp  21331  2idlcpblrng  21542  prmidlnr  21597  qsidomlem2  21614  evlsval3  22375  mpff  22398  mpfaddcl  22399  mpfmulcl  22400  mpfind  22401  pf1rcl  22644  mpfpf1  22646  mdetunilem2  22905  mdetunilem5  22908  mdetunilem6  22909  chfacfisfcpmat  23150  pnfnei  23515  cnptop2  23538  lmcl  23592  lmcnp  23599  flimfil  24265  tlmlmod  24485  ustbasel  24503  ustincl  24504  ustinvel  24506  ustfilxp  24509  tusunif  24564  imasdsf1olem  24669  xmeter  24729  tmsds  24780  metustexhalf  24852  nlmlmod  24974  qdensere  25065  blcvx  25094  tgqioo  25096  icccmplem2  25120  reconnlem1  25123  cnmpopc  25226  phtpcer  25293  phtpcco2  25297  pcohtpylem  25317  pcohtpy  25318  pcophtb  25327  om1addcl  25331  pi1blem  25337  pi1cpbl  25342  pi1grplem  25347  pi1inv  25350  pi1xfrf  25351  pi1xfr  25353  pi1xfrcnvlem  25354  pi1cof  25357  pi1coghm  25359  cphnlm  25470  cphsqrtcl2  25484  tcphcph  25535  lmcau  25611  bcthlem4  25625  minveclem4c  25723  minveclem2  25724  minveclem3b  25726  minveclem4  25730  minveclem6  25732  ivthicc  25756  ovolfsval  25768  ovollb2lem  25786  ovolshftlem1  25807  ovolscalem1  25811  ovolicc1  25814  ovolicc2lem2  25816  ovolicc2lem4  25818  ovolicc2lem5  25819  ovolicopnf  25822  ioombl1lem1  25856  ioombl1lem3  25858  ioombl1lem4  25859  uniioovol  25877  uniioombllem2a  25880  uniioombllem2  25881  uniioombllem3a  25882  uniioombllem3  25883  uniioombllem4  25884  uniioombllem6  25886  dyadmaxlem  25895  volivth  25905  vitalilem2  25907  vitalilem5  25910  i1frn  25975  itg2monolem1  26048  itgcnlem  26087  itgrevallem1  26092  itgreval  26094  itgle  26107  ibladd  26118  iblabslem  26125  itgspliticc  26134  itgsplitioo  26135  ditgcl  26155  ditgswap  26156  ditgsplitlem  26157  limcdif  26173  limcresi  26182  limccnp  26188  limccnp2  26189  limcco  26190  dvlip  26290  dvlip2  26292  dveq0  26297  dvgt0lem1  26299  dvivthlem1  26305  dvcnvrelem1  26314  dvcnvre  26316  dvfsumlem2  26324  ftc1lem1  26332  ftc1a  26334  ftc1lem4  26336  ftc2ditglem  26342  itgsubstlem  26345  ply1rem  26461  fta1glem1  26463  ig1pdvds  26475  plyrem  26605  facth  26606  fta1lem  26607  vieta1lem1  26612  vieta1lem2  26613  aaliou3lem3  26650  aaliou3lem4  26652  aaliou3lem7  26655  taylfvallem1  26663  tayl0  26668  taylply2  26674  radcnvle  26726  psercnlem2  26730  psercnlem1  26731  psercn  26732  pserdvlem1  26733  pserdvlem2  26734  abelth2  26748  coseq00topi  26810  coseq0negpitopi  26811  cosordlem  26837  tanord1  26844  efif1olem1  26849  loglesqrt  27068  logreclem  27069  relogbval  27079  nnlogbexp  27088  chordthmlem4  27142  quart1  27163  quartlem2  27165  quartlem3  27166  quartlem4  27167  quart  27168  acosbnd  27207  atancj  27217  atanlogsublem  27222  atantan  27230  atanbndlem  27232  dvatan  27242  atantayl  27244  rlimcnp2  27273  divsqrtsumlem  27286  ftalem5  27383  ftalem7  27385  basellem4  27390  basellem5  27391  perfectlem2  27536  dchrinv  27567  chpdifbndlem1  27859  pntibndlem2  27897  pntlemc  27901  pntlema  27902  pntlemb  27903  pntlemg  27904  pntlemh  27905  pntlemq  27907  pntlemr  27908  pntlemj  27909  pntlemi  27910  pntlemf  27911  pntlemk  27912  pntlemo  27913  pntleme  27914  pntlem3  27915  pntleml  27917  abvcxp  27921  flt4lem5f  27966  flt4lem7  27968  nna4b4nsq  27969  cutsun12  28155  lesrec  28164  eqcuts3  28169  cofcut2  28287  cofcutr  28289  cofcutrtime  28292  cutmax  28299  cutmin  28300  addsproplem4  28337  addsproplem6  28339  addsuniflem  28366  addsasslem1  28368  addsasslem2  28369  negsproplem5  28397  negsproplem6  28398  negcut2  28405  negsunif  28420  mulsproplem12  28492  sltmuls1  28512  sltmuls2  28513  mulsuniflem  28514  precsexlem11  28582  twocut  28788  pw2cut2  28827  axtgpasch  28908  cgr3simp2  28963  legso  29041  hlne2  29051  hlln  29052  mirhl  29130  inagswap  29339  inagne2  29341  dfcgrg2  29387  subumgredg2  29845  upgrres1  29873  nb3grprlem1  29940  wlkp  30176  subgrwlk  30248  spthcycl  30371  wspthsswwlkn  30486  2wlkdlem6  30499  clwwisshclwwsn  30586  erclwwlkeqlen  30589  erclwwlksym  30591  erclwwlktr  30592  clwwlkn  30596  clwwlknwrd  30604  clwwlknonex2e  30680  acycgrcycl  30732  grpoass  31084  vcsm  31143  nvf  31241  ssps  31311  minvecolem2  31456  minvecolem4c  31460  minvecolem4  31461  minvecolem5  31462  minvecolem6  31463  eigvec1  32543  eliccelico  33348  elicoelioo  33349  pmtrto1cl  33639  cyc3evpm  33690  slmdvsdi  33755  slmdvs1  33760  sdrgdvcl  33840  sdrginvcl  33841  fldgenssp  33859  imaslmod  33893  mxidlnr  33968  0ringmon1p  34068  irngnzply1lem  34301  irngnzply1  34302  ply1annig1p  34315  minplycl  34317  ply1annprmidl  34318  minplym1p  34324  minplynzm1p  34325  algextdeglem1  34328  algextdeglem2  34329  algextdeglem3  34330  algextdeglem4  34331  algextdeglem5  34332  constrsqrtcl  34390  cnre2csqlem  34521  lmxrge0  34563  sigaclci  34743  difunielsiga  34744  insiga  34749  ldsysgenld  34772  sigapildsyslem  34773  sigapildsys  34774  ldgenpisyslem1  34775  measvnul  34818  sibfrn  34949  eulerpartlemt  34983  eulerpartlemmf  34987  tg5segofs  35285  lpadleft  35295  subfacp1lem2a  35911  subfacp1lem3  35913  subfacp1lem4  35914  subfacp1lem5  35915  sconnpht2  35969  sconnpi1  35970  resconn  35977  cvmsss  35998  cvmsn0  35999  cvmlift2lem3  36036  cvmlift2lem7  36040  cvmliftphtlem  36048  cvmliftpht  36049  cvmlift3lem5  36054  cvmlift3lem6  36055  msrf  36273  elmsta  36279  mclsax  36300  mthmpps  36313  mclspps  36315  ivthALT  37090  weiunpo  37220  weiunso  37221  weiunfr  37222  weiunse  37223  poimirlem17  38520  poimirlem20  38523  ibladdnc  38560  iblabsnclem  38566  ftc1cnnclem  38574  ftc1anc  38584  ftc2nc  38585  heiborlem3  38712  iccbnd  38739  rngohom1  38867  idl0cl  38917  maxidlnr  38941  lshpne  40004  opococ  40217  opexmid  40229  hlclat  40380  lclkrslem2  42560  fzne2d  42995  dvrelog2  43079  dvrelog3  43080  0nonelalab  43082  aks4d1p1p5  43090  primrootsunit1  43112  primrootscoprmpow  43114  primrootscoprbij  43117  primrootspoweq0  43121  aks6d1c2lem3  43141  aks6d1c2  43145  aks6d1c6lem5  43192  aks5lem1  43201  aks5lem2  43202  aks5lem3a  43204  aks5lem5a  43206  unitscyglem1  43210  gneispacern2  45095  cvgdvgrat  45253  iccshift  46471  iccsuble  46472  icoiccdif  46477  mullimc  46569  limccog  46573  mullimcf  46576  lptioo2  46584  limcmptdm  46586  limcicciooub  46588  xlimmnfvlem1  46783  xlimpnfvlem1  46787  icccncfext  46838  cncfioobdlem  46847  ditgeqiooicc  46911  itgsubsticc  46927  iblcncfioo  46929  itgiccshift  46931  itgperiod  46932  itgsbtaddcnst  46933  stoweidlem31  46982  stoweidlem36  46987  stoweidlem38  46989  stoweidlem44  46995  stoweidlem62  47013  dirkercncflem1  47054  dirkercncflem4  47057  fourierdlem26  47084  fourierdlem32  47090  fourierdlem33  47091  fourierdlem37  47095  fourierdlem42  47100  fourierdlem54  47111  fourierdlem63  47120  fourierdlem64  47121  fourierdlem65  47122  fourierdlem69  47126  fourierdlem74  47131  fourierdlem75  47132  fourierdlem79  47136  fourierdlem81  47138  fourierdlem82  47139  fourierdlem89  47146  fourierdlem90  47147  fourierdlem91  47148  fourierdlem93  47150  fourierdlem101  47158  fourierdlem111  47168  saldifcl  47270  unisalgen2  47305  hoidmv1lelem3  47544  smff  47683  sigardiv  47812  sigarcol  47815  sharhght  47816  sigaradd  47817  cevathlem1  47818  cevathlem2  47819  cevath  47820  proththd  48640  perfectALTVlem2  48761  gpgnbgrvtx0  49113  gpgnbgrvtx1  49114  imasubc2  50201  imaf1co  50204  idfullsubc  50210  fucofulem1  50359  rr3fv2cld  50889