Theorem simp2d 1143

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp2bi  1146  f1dom3fv3dif  7243  f1dom3el3dif  7244  f1prex  7259  oeeui  8566  resixp  8906  domssex  9102  cantnflem1a  9638  cantnflem1d  9641  cantnflem3  9644  cantnflem4  9645  fpwwe2lem6  10589  canthnumlem  10601  canthp1lem2  10606  wun0  10671  lelttrdi  11336  supmullem2  12154  supmul  12155  ixxdisj  13321  ixxun  13322  ixxss1  13324  ixxss2  13325  ixxss12  13326  ixxub  13327  ixxlb  13328  ubioo  13338  elicore  13359  iccgelb  13363  iccss2  13378  icodisj  13437  xov1plusxeqvd  13459  fldiv  13822  immul  15102  sqrtge0  15223  sqrtrege0  15332  icco1  15506  ruclem2  16200  ruclem3  16201  ruclem8  16205  ruclem12  16209  gcddvds  16473  crth  16748  phimullem  16749  eulerthlem1  16751  eulerthlem2  16752  prmreclem3  16889  sectcan  17717  sectco  17718  sectmon  17744  monsect  17745  funcixp  17829  funcsect  17834  invfuc  17939  coapm  18033  catciso  18073  posasymb  18280  ipodrsima  18500  pstr2  18530  psdmrn  18532  psref  18533  mhmlin  18720  subm0cl  18738  eqger  19110  eqgcpbl  19114  gaorber  19240  orbstafun  19243  cayleyth  19345  pmtrrn2  19390  pmtrfinv  19391  dfod2  19494  sylow2blem1  19550  dprdf  19938  dprdff  19944  dprdfcl  19945  dprdsplit  19980  dpjcntz  19984  ablfac1a  20001  ablfac1b  20002  lmodvsdi  20791  lbssp  20986  2idlcpblrng  21181  mpff  22011  mpfaddcl  22012  mpfmulcl  22013  mpfind  22014  pf1rcl  22236  mpfpf1  22238  mdetunilem2  22500  mdetunilem5  22503  mdetunilem6  22504  chfacfisfcpmat  22742  pnfnei  23107  cnptop2  23130  lmcl  23184  lmcnp  23191  flimfil  23856  tlmlmod  24076  ustbasel  24094  ustincl  24095  ustinvel  24097  ustfilxp  24100  tusunif  24156  imasdsf1olem  24261  xmeter  24321  tmsds  24372  metustexhalf  24444  nlmlmod  24566  qdensere  24657  blcvx  24686  tgqioo  24688  icccmplem2  24712  reconnlem1  24715  cnmpopc  24822  phtpcer  24894  phtpcco2  24899  pcohtpylem  24919  pcohtpy  24920  pcophtb  24929  om1addcl  24933  pi1blem  24939  pi1cpbl  24944  pi1grplem  24949  pi1inv  24952  pi1xfrf  24953  pi1xfr  24955  pi1xfrcnvlem  24956  pi1cof  24959  pi1coghm  24961  cphnlm  25072  cphsqrtcl2  25086  tcphcph  25137  lmcau  25213  bcthlem4  25227  minveclem4c  25325  minveclem2  25326  minveclem3b  25328  minveclem4  25332  minveclem6  25334  ivthicc  25359  ovolfsval  25371  ovollb2lem  25389  ovolshftlem1  25410  ovolscalem1  25414  ovolicc1  25417  ovolicc2lem2  25419  ovolicc2lem4  25421  ovolicc2lem5  25422  ovolicopnf  25425  ioombl1lem1  25459  ioombl1lem3  25461  ioombl1lem4  25462  uniioovol  25480  uniioombllem2a  25483  uniioombllem2  25484  uniioombllem3a  25485  uniioombllem3  25486  uniioombllem4  25487  uniioombllem6  25489  dyadmaxlem  25498  volivth  25508  vitalilem2  25510  vitalilem5  25513  i1frn  25578  itg2monolem1  25651  itgcnlem  25691  itgrevallem1  25696  itgreval  25698  itgle  25711  ibladd  25722  iblabslem  25729  itgspliticc  25738  itgsplitioo  25739  ditgcl  25759  ditgswap  25760  ditgsplitlem  25761  limcdif  25777  limcresi  25786  limccnp  25792  limccnp2  25793  limcco  25794  dvlip  25898  dvlip2  25900  dveq0  25905  dvgt0lem1  25907  dvivthlem1  25913  dvcnvrelem1  25922  dvcnvre  25924  dvfsumlem2  25933  dvfsumlem2OLD  25934  ftc1lem1  25942  ftc1a  25944  ftc1lem4  25946  ftc2ditglem  25952  itgsubstlem  25955  ply1rem  26071  fta1glem1  26073  ig1pdvds  26085  plyrem  26213  facth  26214  fta1lem  26215  vieta1lem1  26218  vieta1lem2  26219  aaliou3lem3  26252  aaliou3lem4  26254  aaliou3lem7  26257  taylfvallem1  26264  tayl0  26269  taylply2  26275  taylply2OLD  26276  radcnvle  26329  psercnlem2  26334  psercnlem1  26335  psercn  26336  pserdvlem1  26337  pserdvlem2  26338  abelth2  26352  coseq00topi  26411  coseq0negpitopi  26412  cosordlem  26439  tanord1  26446  efif1olem1  26451  loglesqrt  26671  logreclem  26672  relogbval  26682  nnlogbexp  26691  chordthmlem4  26745  quart1  26766  quartlem2  26768  quartlem3  26769  quartlem4  26770  quart  26771  acosbnd  26810  atancj  26820  atanlogsublem  26825  atantan  26833  atanbndlem  26835  dvatan  26845  atantayl  26847  rlimcnp2  26876  divsqrtsumlem  26890  ftalem5  26987  ftalem7  26989  basellem4  26994  basellem5  26995  perfectlem2  27141  dchrinv  27172  chpdifbndlem1  27464  pntibndlem2  27502  pntlemc  27506  pntlema  27507  pntlemb  27508  pntlemg  27509  pntlemh  27510  pntlemq  27512  pntlemr  27513  pntlemj  27514  pntlemi  27515  pntlemf  27516  pntlemk  27517  pntlemo  27518  pntleme  27519  pntlem3  27520  pntleml  27522  abvcxp  27526  scutun12  27722  slerec  27731  cofcut2  27830  cofcutr  27832  cofcutrtime  27835  cutmax  27842  cutmin  27843  addsproplem4  27879  addsproplem6  27881  addsuniflem  27908  addsasslem1  27910  addsasslem2  27911  negsproplem5  27938  negsproplem6  27939  negscut2  27946  negsunif  27961  mulsproplem12  28030  ssltmul1  28050  ssltmul2  28051  mulsuniflem  28052  precsexlem11  28119  twocut  28309  axtgpasch  28394  cgr3simp2  28448  legso  28526  hlne2  28533  hlln  28534  mirhl  28606  inagswap  28768  inagne2  28770  dfcgrg2  28790  subumgredg2  29212  upgrres1  29240  nb3grprlem1  29307  wlkp  29544  wspthsswwlkn  29848  2wlkdlem6  29861  clwwisshclwwsn  29945  erclwwlkeqlen  29948  erclwwlksym  29950  erclwwlktr  29951  clwwlkn  29955  clwwlknwrd  29963  clwwlknonex2e  30039  grpoass  30432  vcsm  30491  nvf  30589  ssps  30659  minvecolem2  30804  minvecolem4c  30808  minvecolem4  30809  minvecolem5  30810  minvecolem6  30811  eigvec1  31891  eliccelico  32700  elicoelioo  32701  pmtrto1cl  33056  cyc3evpm  33107  slmdvsdi  33168  slmdvs1  33173  sdrgdvcl  33249  sdrginvcl  33250  fldgenssp  33268  imaslmod  33324  prmidlnr  33410  qsidomlem2  33424  mxidlnr  33435  0ringmon1p  33526  irngnzply1lem  33685  irngnzply1  33686  ply1annig1p  33694  minplycl  33696  ply1annprmidl  33697  minplym1p  33703  minplynzm1p  33704  algextdeglem1  33707  algextdeglem2  33708  algextdeglem3  33709  algextdeglem4  33710  algextdeglem5  33711  constrsqrtcl  33769  cnre2csqlem  33900  lmxrge0  33942  sigaclci  34122  difelsiga  34123  insiga  34127  ldsysgenld  34150  sigapildsyslem  34151  sigapildsys  34152  ldgenpisyslem1  34153  measvnul  34196  sibfrn  34328  eulerpartlemt  34362  eulerpartlemmf  34366  tg5segofs  34664  lpadleft  34674  spthcycl  35116  subgrwlk  35119  acycgrcycl  35134  subfacp1lem2a  35167  subfacp1lem3  35169  subfacp1lem4  35170  subfacp1lem5  35171  sconnpht2  35225  sconnpi1  35226  resconn  35233  cvmsss  35254  cvmsn0  35255  cvmlift2lem3  35292  cvmlift2lem7  35296  cvmliftphtlem  35304  cvmliftpht  35305  cvmlift3lem5  35310  cvmlift3lem6  35311  msrf  35529  elmsta  35535  mclsax  35556  mthmpps  35569  mclspps  35571  ivthALT  36323  weiunpo  36453  weiunso  36454  weiunfr  36455  weiunse  36456  poimirlem17  37631  poimirlem20  37634  ibladdnc  37671  iblabsnclem  37677  ftc1cnnclem  37685  ftc1anc  37695  ftc2nc  37696  heiborlem3  37807  iccbnd  37834  rngohom1  37962  idl0cl  38012  maxidlnr  38036  lshpne  38975  opococ  39188  opexmid  39200  hlclat  39351  lclkrslem2  41532  fzne2d  41968  dvrelog2  42052  dvrelog3  42053  0nonelalab  42055  aks4d1p1p5  42063  primrootsunit1  42085  primrootscoprmpow  42087  primrootscoprbij  42090  primrootspoweq0  42094  aks6d1c2lem3  42114  aks6d1c2  42118  aks6d1c6lem5  42165  aks5lem1  42174  aks5lem2  42175  aks5lem3a  42177  aks5lem5a  42179  unitscyglem1  42183  evlsval3  42547  flt4lem5f  42645  flt4lem7  42647  nna4b4nsq  42648  gneispacern2  44128  cvgdvgrat  44302  iccshift  45516  iccsuble  45517  icoiccdif  45522  mullimc  45614  limccog  45618  mullimcf  45621  lptioo2  45629  limcmptdm  45633  limcicciooub  45635  xlimmnfvlem1  45830  xlimpnfvlem1  45834  icccncfext  45885  cncfioobdlem  45894  ditgeqiooicc  45958  itgsubsticc  45974  iblcncfioo  45976  itgiccshift  45978  itgperiod  45979  itgsbtaddcnst  45980  stoweidlem31  46029  stoweidlem36  46034  stoweidlem38  46036  stoweidlem44  46042  stoweidlem62  46060  dirkercncflem1  46101  dirkercncflem4  46104  fourierdlem26  46131  fourierdlem32  46137  fourierdlem33  46138  fourierdlem37  46142  fourierdlem42  46147  fourierdlem54  46158  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem69  46173  fourierdlem74  46178  fourierdlem75  46179  fourierdlem79  46183  fourierdlem81  46185  fourierdlem82  46186  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem93  46197  fourierdlem101  46205  fourierdlem111  46215  saldifcl  46317  unisalgen2  46352  hoidmv1lelem3  46591  smff  46730  sigardiv  46859  sigarcol  46862  sharhght  46863  sigaradd  46864  cevathlem1  46865  cevathlem2  46866  cevath  46867  proththd  47615  perfectALTVlem2  47723  gpgnbgrvtx0  48065  gpgnbgrvtx1  48066  imasubc2  49141  imaf1co  49144  idfullsubc  49150  fucofulem1  49299