Theorem simp2d 1141

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  simp2bi  1144  f1dom3fv3dif  7122  f1dom3el3dif  7123  f1prex  7136  oeeui  8395  resixp  8679  domssex  8874  cantnflem1a  9373  cantnflem1d  9376  cantnflem3  9379  cantnflem4  9380  fpwwe2lem6  10323  canthnumlem  10335  canthp1lem2  10340  wun0  10405  lelttrdi  11067  supmullem2  11876  supmul  11877  ixxdisj  13023  ixxun  13024  ixxss1  13026  ixxss2  13027  ixxss12  13028  ixxub  13029  ixxlb  13030  ubioo  13040  elicore  13060  iccgelb  13064  iccss2  13079  icodisj  13137  xov1plusxeqvd  13159  fldiv  13508  immul  14775  sqrtge0  14897  sqrtrege0  15005  icco1  15177  ruclem2  15869  ruclem3  15870  ruclem8  15874  ruclem12  15878  gcddvds  16138  crth  16407  phimullem  16408  eulerthlem1  16410  eulerthlem2  16411  prmreclem3  16547  sectcan  17384  sectco  17385  sectmon  17411  monsect  17412  funcixp  17498  funcsect  17503  invfuc  17608  coapm  17702  catciso  17742  posasymb  17952  ipodrsima  18174  pstr2  18204  psdmrn  18206  psref  18207  mhmlin  18352  subm0cl  18365  eqger  18721  eqgcpbl  18725  gaorber  18829  orbstafun  18832  cayleyth  18938  pmtrrn2  18983  pmtrfinv  18984  dfod2  19086  sylow2blem1  19140  dprdf  19524  dprdff  19530  dprdfcl  19531  dprdsplit  19566  dpjcntz  19570  ablfac1a  19587  ablfac1b  19588  lmodvsdi  20061  lbssp  20256  2idlcpbl  20418  assaring  20978  mpff  21224  mpfaddcl  21225  mpfmulcl  21226  mpfind  21227  pf1rcl  21425  mpfpf1  21427  mdetunilem2  21670  mdetunilem5  21673  mdetunilem6  21674  chfacfisfcpmat  21912  pnfnei  22279  cnptop2  22302  lmcl  22356  lmcnp  22363  flimfil  23028  tlmlmod  23248  ustbasel  23266  ustincl  23267  ustinvel  23269  ustfilxp  23272  tusunif  23329  imasdsf1olem  23434  xmeter  23494  tmsds  23546  metustexhalf  23618  nlmlmod  23748  qdensere  23839  blcvx  23867  tgqioo  23869  icccmplem2  23892  reconnlem1  23895  cnmpopc  23997  phtpcer  24064  phtpcco2  24068  pcohtpylem  24088  pcohtpy  24089  pcophtb  24098  om1addcl  24102  pi1blem  24108  pi1cpbl  24113  pi1grplem  24118  pi1inv  24121  pi1xfrf  24122  pi1xfr  24124  pi1xfrcnvlem  24125  pi1cof  24128  pi1coghm  24130  cphnlm  24241  cphsqrtcl2  24255  tcphcph  24306  lmcau  24382  bcthlem4  24396  minveclem4c  24494  minveclem2  24495  minveclem3b  24497  minveclem4  24501  minveclem6  24503  ivthicc  24527  ovolfsval  24539  ovollb2lem  24557  ovolshftlem1  24578  ovolscalem1  24582  ovolicc1  24585  ovolicc2lem2  24587  ovolicc2lem4  24589  ovolicc2lem5  24590  ovolicopnf  24593  ioombl1lem1  24627  ioombl1lem3  24629  ioombl1lem4  24630  uniioovol  24648  uniioombllem2a  24651  uniioombllem2  24652  uniioombllem3a  24653  uniioombllem3  24654  uniioombllem4  24655  uniioombllem6  24657  dyadmaxlem  24666  volivth  24676  vitalilem2  24678  vitalilem5  24681  i1frn  24746  itg2monolem1  24820  itgcnlem  24859  itgrevallem1  24864  itgreval  24866  itgle  24879  ibladd  24890  iblabslem  24897  itgspliticc  24906  itgsplitioo  24907  ditgcl  24927  ditgswap  24928  ditgsplitlem  24929  limcdif  24945  limcresi  24954  limccnp  24960  limccnp2  24961  limcco  24962  dvlip  25062  dvlip2  25064  dveq0  25069  dvgt0lem1  25071  dvivthlem1  25077  dvcnvrelem1  25086  dvcnvre  25088  dvfsumlem2  25096  ftc1lem1  25104  ftc1a  25106  ftc1lem4  25108  ftc2ditglem  25114  itgsubstlem  25117  ply1rem  25233  fta1glem1  25235  ig1pdvds  25246  plyrem  25370  facth  25371  fta1lem  25372  vieta1lem1  25375  vieta1lem2  25376  aaliou3lem3  25409  aaliou3lem4  25411  aaliou3lem7  25414  taylfvallem1  25421  tayl0  25426  taylply2  25432  radcnvle  25484  psercnlem2  25488  psercnlem1  25489  psercn  25490  pserdvlem1  25491  pserdvlem2  25492  abelth2  25506  coseq00topi  25564  coseq0negpitopi  25565  cosordlem  25591  tanord1  25598  efif1olem1  25603  loglesqrt  25816  logreclem  25817  relogbval  25827  nnlogbexp  25836  chordthmlem4  25890  quart1  25911  quartlem2  25913  quartlem3  25914  quartlem4  25915  quart  25916  acosbnd  25955  atancj  25965  atanlogsublem  25970  atantan  25978  atanbndlem  25980  dvatan  25990  atantayl  25992  rlimcnp2  26021  divsqrtsumlem  26034  ftalem5  26131  ftalem7  26133  basellem4  26138  basellem5  26139  perfectlem2  26283  dchrinv  26314  chpdifbndlem1  26606  pntibndlem2  26644  pntlemc  26648  pntlema  26649  pntlemb  26650  pntlemg  26651  pntlemh  26652  pntlemq  26654  pntlemr  26655  pntlemj  26656  pntlemi  26657  pntlemf  26658  pntlemk  26659  pntlemo  26660  pntleme  26661  pntlem3  26662  pntleml  26664  abvcxp  26668  axtgpasch  26732  cgr3simp2  26786  legso  26864  hlne2  26871  hlln  26872  mirhl  26944  inagswap  27106  inagne2  27108  dfcgrg2  27128  subumgredg2  27555  upgrres1  27583  nb3grprlem1  27650  wlkp  27886  wspthsswwlkn  28184  2wlkdlem6  28197  clwwisshclwwsn  28281  erclwwlkeqlen  28284  erclwwlksym  28286  erclwwlktr  28287  clwwlkn  28291  clwwlknwrd  28299  clwwlknonex2e  28375  grpoass  28766  vcsm  28825  nvf  28923  ssps  28993  minvecolem2  29138  minvecolem4c  29142  minvecolem4  29143  minvecolem5  29144  minvecolem6  29145  eigvec1  30225  eliccelico  31000  elicoelioo  31001  pmtrto1cl  31268  cyc3evpm  31319  slmdvsdi  31370  slmdvs1  31375  imaslmod  31455  prmidlnr  31516  qsidomlem2  31531  mxidlnr  31538  cnre2csqlem  31762  lmxrge0  31804  sigaclci  32000  difelsiga  32001  insiga  32005  ldsysgenld  32028  sigapildsyslem  32029  sigapildsys  32030  ldgenpisyslem1  32031  measvnul  32074  sibfrn  32204  eulerpartlemt  32238  eulerpartlemmf  32242  tg5segofs  32553  lpadleft  32563  spthcycl  32991  subgrwlk  32994  acycgrcycl  33009  subfacp1lem2a  33042  subfacp1lem3  33044  subfacp1lem4  33045  subfacp1lem5  33046  sconnpht2  33100  sconnpi1  33101  resconn  33108  cvmsss  33129  cvmsn0  33130  cvmlift2lem3  33167  cvmlift2lem7  33171  cvmliftphtlem  33179  cvmliftpht  33180  cvmlift3lem5  33185  cvmlift3lem6  33186  msrf  33404  elmsta  33410  mclsax  33431  mthmpps  33444  mclspps  33446  scutun12  33931  slerec  33940  cofcut2  34018  cofcutr  34019  cofcutrtime  34020  ivthALT  34451  poimirlem17  35721  poimirlem20  35724  ibladdnc  35761  iblabsnclem  35767  ftc1cnnclem  35775  ftc1anc  35785  ftc2nc  35786  heiborlem3  35898  iccbnd  35925  rngohom1  36053  idl0cl  36103  maxidlnr  36127  lshpne  36923  opococ  37136  opexmid  37148  hlclat  37299  lclkrslem2  39479  fzne2d  39917  dvrelog2  40000  dvrelog3  40001  0nonelalab  40003  aks4d1p1p5  40011  metakunt8  40060  metakunt21  40073  metakunt22  40074  metakunt24  40076  metakunt25  40077  evlsval3  40195  flt4lem5f  40410  flt4lem7  40412  nna4b4nsq  40413  gneispacern2  41638  cvgdvgrat  41820  iccshift  42946  iccsuble  42947  icoiccdif  42952  mullimc  43047  limccog  43051  mullimcf  43054  lptioo2  43062  limcmptdm  43066  limcicciooub  43068  xlimmnfvlem1  43263  xlimpnfvlem1  43267  icccncfext  43318  cncfioobdlem  43327  ditgeqiooicc  43391  itgsubsticc  43407  iblcncfioo  43409  itgiccshift  43411  itgperiod  43412  itgsbtaddcnst  43413  stoweidlem31  43462  stoweidlem36  43467  stoweidlem38  43469  stoweidlem44  43475  stoweidlem62  43493  dirkercncflem1  43534  dirkercncflem4  43537  fourierdlem26  43564  fourierdlem32  43570  fourierdlem33  43571  fourierdlem37  43575  fourierdlem42  43580  fourierdlem54  43591  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem69  43606  fourierdlem74  43611  fourierdlem75  43612  fourierdlem79  43616  fourierdlem81  43618  fourierdlem82  43619  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem93  43630  fourierdlem101  43638  fourierdlem111  43648  saldifcl  43750  unisalgen2  43783  hoidmv1lelem3  44021  smff  44155  smfpimltxr  44170  sigardiv  44264  sigarcol  44267  sharhght  44268  sigaradd  44269  cevathlem1  44270  cevathlem2  44271  cevath  44272  proththd  44954  perfectALTVlem2  45062