Theorem simp2d 1149

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simp2bi  1152  f1dom3fv3dif  7219  f1dom3el3dif  7220  f1prex  7235  oeeui  8535  resixp  8878  domssex  9073  cantnflem1a  9604  cantnflem1d  9607  cantnflem3  9610  cantnflem4  9611  fpwwe2lem6  10557  canthnumlem  10569  canthp1lem2  10574  wun0  10639  lelttrdi  11306  supmullem2  12125  supmul  12126  ixxdisj  13311  ixxun  13312  ixxss1  13314  ixxss2  13315  ixxss12  13316  ixxub  13317  ixxlb  13318  ubioo  13328  elicore  13349  iccgelb  13353  iccss2  13368  icodisj  13427  xov1plusxeqvd  13449  fldiv  13817  immul  15096  sqrtge0  15217  sqrtrege0  15326  icco1  15500  ruclem2  16197  ruclem3  16198  ruclem8  16202  ruclem12  16206  gcddvds  16470  crth  16746  phimullem  16747  eulerthlem1  16749  eulerthlem2  16750  prmreclem3  16887  sectcan  17720  sectco  17721  sectmon  17747  monsect  17748  funcixp  17832  funcsect  17837  invfuc  17942  coapm  18036  catciso  18076  posasymb  18283  ipodrsima  18505  pstr2  18535  psdmrn  18537  psref  18538  mhmlin  18759  subm0cl  18777  eqger  19151  eqgcpbl  19155  gaorber  19281  orbstafun  19284  cayleyth  19388  pmtrrn2  19433  pmtrfinv  19434  dfod2  19537  sylow2blem1  19593  dprdf  19981  dprdff  19987  dprdfcl  19988  dprdsplit  20023  dpjcntz  20027  ablfac1a  20044  ablfac1b  20045  lmodvsdi  20882  lbssp  21076  2idlcpblrng  21271  evlsval3  22072  mpff  22095  mpfaddcl  22096  mpfmulcl  22097  mpfind  22098  pf1rcl  22342  mpfpf1  22344  mdetunilem2  22603  mdetunilem5  22606  mdetunilem6  22607  chfacfisfcpmat  22845  pnfnei  23210  cnptop2  23233  lmcl  23287  lmcnp  23294  flimfil  23959  tlmlmod  24179  ustbasel  24197  ustincl  24198  ustinvel  24200  ustfilxp  24203  tusunif  24258  imasdsf1olem  24363  xmeter  24423  tmsds  24474  metustexhalf  24546  nlmlmod  24668  qdensere  24759  blcvx  24788  tgqioo  24790  icccmplem2  24814  reconnlem1  24817  cnmpopc  24920  phtpcer  24987  phtpcco2  24991  pcohtpylem  25011  pcohtpy  25012  pcophtb  25021  om1addcl  25025  pi1blem  25031  pi1cpbl  25036  pi1grplem  25041  pi1inv  25044  pi1xfrf  25045  pi1xfr  25047  pi1xfrcnvlem  25048  pi1cof  25051  pi1coghm  25053  cphnlm  25164  cphsqrtcl2  25178  tcphcph  25229  lmcau  25305  bcthlem4  25319  minveclem4c  25417  minveclem2  25418  minveclem3b  25420  minveclem4  25424  minveclem6  25426  ivthicc  25450  ovolfsval  25462  ovollb2lem  25480  ovolshftlem1  25501  ovolscalem1  25505  ovolicc1  25508  ovolicc2lem2  25510  ovolicc2lem4  25512  ovolicc2lem5  25513  ovolicopnf  25516  ioombl1lem1  25550  ioombl1lem3  25552  ioombl1lem4  25553  uniioovol  25571  uniioombllem2a  25574  uniioombllem2  25575  uniioombllem3a  25576  uniioombllem3  25577  uniioombllem4  25578  uniioombllem6  25580  dyadmaxlem  25589  volivth  25599  vitalilem2  25601  vitalilem5  25604  i1frn  25669  itg2monolem1  25742  itgcnlem  25782  itgrevallem1  25787  itgreval  25789  itgle  25802  ibladd  25813  iblabslem  25820  itgspliticc  25829  itgsplitioo  25830  ditgcl  25850  ditgswap  25851  ditgsplitlem  25852  limcdif  25868  limcresi  25877  limccnp  25883  limccnp2  25884  limcco  25885  dvlip  25985  dvlip2  25987  dveq0  25992  dvgt0lem1  25994  dvivthlem1  26000  dvcnvrelem1  26009  dvcnvre  26011  dvfsumlem2  26019  ftc1lem1  26027  ftc1a  26029  ftc1lem4  26031  ftc2ditglem  26037  itgsubstlem  26040  ply1rem  26156  fta1glem1  26158  ig1pdvds  26170  plyrem  26296  facth  26297  fta1lem  26298  vieta1lem1  26301  vieta1lem2  26302  aaliou3lem3  26335  aaliou3lem4  26337  aaliou3lem7  26340  taylfvallem1  26347  tayl0  26352  taylply2  26358  radcnvle  26410  psercnlem2  26414  psercnlem1  26415  psercn  26416  pserdvlem1  26417  pserdvlem2  26418  abelth2  26432  coseq00topi  26491  coseq0negpitopi  26492  cosordlem  26519  tanord1  26526  efif1olem1  26531  loglesqrt  26750  logreclem  26751  relogbval  26761  nnlogbexp  26770  chordthmlem4  26824  quart1  26845  quartlem2  26847  quartlem3  26848  quartlem4  26849  quart  26850  acosbnd  26889  atancj  26899  atanlogsublem  26904  atantan  26912  atanbndlem  26914  dvatan  26924  atantayl  26926  rlimcnp2  26955  divsqrtsumlem  26968  ftalem5  27065  ftalem7  27067  basellem4  27072  basellem5  27073  perfectlem2  27218  dchrinv  27249  chpdifbndlem1  27541  pntibndlem2  27579  pntlemc  27583  pntlema  27584  pntlemb  27585  pntlemg  27586  pntlemh  27587  pntlemq  27589  pntlemr  27590  pntlemj  27591  pntlemi  27592  pntlemf  27593  pntlemk  27594  pntlemo  27595  pntleme  27596  pntlem3  27597  pntleml  27599  abvcxp  27603  cutsun12  27807  lesrec  27816  eqcuts3  27821  cofcut2  27939  cofcutr  27941  cofcutrtime  27944  cutmax  27951  cutmin  27952  addsproplem4  27989  addsproplem6  27991  addsuniflem  28018  addsasslem1  28020  addsasslem2  28021  negsproplem5  28049  negsproplem6  28050  negcut2  28057  negsunif  28072  mulsproplem12  28144  sltmuls1  28164  sltmuls2  28165  mulsuniflem  28166  precsexlem11  28234  twocut  28440  pw2cut2  28479  axtgpasch  28560  cgr3simp2  28614  legso  28692  hlne2  28699  hlln  28700  mirhl  28772  inagswap  28934  inagne2  28936  dfcgrg2  28956  subumgredg2  29379  upgrres1  29407  nb3grprlem1  29474  wlkp  29710  wspthsswwlkn  30011  2wlkdlem6  30024  clwwisshclwwsn  30111  erclwwlkeqlen  30114  erclwwlksym  30116  erclwwlktr  30117  clwwlkn  30121  clwwlknwrd  30129  clwwlknonex2e  30205  grpoass  30599  vcsm  30658  nvf  30756  ssps  30826  minvecolem2  30971  minvecolem4c  30975  minvecolem4  30976  minvecolem5  30977  minvecolem6  30978  eigvec1  32058  eliccelico  32876  elicoelioo  32877  pmtrto1cl  33187  cyc3evpm  33238  slmdvsdi  33303  slmdvs1  33308  sdrgdvcl  33390  sdrginvcl  33391  fldgenssp  33409  imaslmod  33443  prmidlnr  33529  qsidomlem2  33543  mxidlnr  33554  0ringmon1p  33647  irngnzply1lem  33881  irngnzply1  33882  ply1annig1p  33895  minplycl  33897  ply1annprmidl  33898  minplym1p  33904  minplynzm1p  33905  algextdeglem1  33908  algextdeglem2  33909  algextdeglem3  33910  algextdeglem4  33911  algextdeglem5  33912  constrsqrtcl  33970  cnre2csqlem  34101  lmxrge0  34143  sigaclci  34323  difelsiga  34324  insiga  34328  ldsysgenld  34351  sigapildsyslem  34352  sigapildsys  34353  ldgenpisyslem1  34354  measvnul  34397  sibfrn  34528  eulerpartlemt  34562  eulerpartlemmf  34566  tg5segofs  34864  lpadleft  34874  spthcycl  35358  subgrwlk  35361  acycgrcycl  35376  subfacp1lem2a  35409  subfacp1lem3  35411  subfacp1lem4  35412  subfacp1lem5  35413  sconnpht2  35467  sconnpi1  35468  resconn  35475  cvmsss  35496  cvmsn0  35497  cvmlift2lem3  35534  cvmlift2lem7  35538  cvmliftphtlem  35546  cvmliftpht  35547  cvmlift3lem5  35552  cvmlift3lem6  35553  msrf  35771  elmsta  35777  mclsax  35798  mthmpps  35811  mclspps  35813  ivthALT  36564  weiunpo  36694  weiunso  36695  weiunfr  36696  weiunse  36697  poimirlem17  38005  poimirlem20  38008  ibladdnc  38045  iblabsnclem  38051  ftc1cnnclem  38059  ftc1anc  38069  ftc2nc  38070  heiborlem3  38181  iccbnd  38208  rngohom1  38336  idl0cl  38386  maxidlnr  38410  lshpne  39475  opococ  39688  opexmid  39700  hlclat  39851  lclkrslem2  42031  fzne2d  42466  dvrelog2  42550  dvrelog3  42551  0nonelalab  42553  aks4d1p1p5  42561  primrootsunit1  42583  primrootscoprmpow  42585  primrootscoprbij  42588  primrootspoweq0  42592  aks6d1c2lem3  42612  aks6d1c2  42616  aks6d1c6lem5  42663  aks5lem1  42672  aks5lem2  42673  aks5lem3a  42675  aks5lem5a  42677  unitscyglem1  42681  flt4lem5f  43108  flt4lem7  43110  nna4b4nsq  43111  gneispacern2  44584  cvgdvgrat  44758  iccshift  45964  iccsuble  45965  icoiccdif  45970  mullimc  46062  limccog  46066  mullimcf  46069  lptioo2  46077  limcmptdm  46079  limcicciooub  46081  xlimmnfvlem1  46276  xlimpnfvlem1  46280  icccncfext  46331  cncfioobdlem  46340  ditgeqiooicc  46404  itgsubsticc  46420  iblcncfioo  46422  itgiccshift  46424  itgperiod  46425  itgsbtaddcnst  46426  stoweidlem31  46475  stoweidlem36  46480  stoweidlem38  46482  stoweidlem44  46488  stoweidlem62  46506  dirkercncflem1  46547  dirkercncflem4  46550  fourierdlem26  46577  fourierdlem32  46583  fourierdlem33  46584  fourierdlem37  46588  fourierdlem42  46593  fourierdlem54  46604  fourierdlem63  46613  fourierdlem64  46614  fourierdlem65  46615  fourierdlem69  46619  fourierdlem74  46624  fourierdlem75  46625  fourierdlem79  46629  fourierdlem81  46631  fourierdlem82  46632  fourierdlem89  46639  fourierdlem90  46640  fourierdlem91  46641  fourierdlem93  46643  fourierdlem101  46651  fourierdlem111  46661  saldifcl  46763  unisalgen2  46798  hoidmv1lelem3  47037  smff  47176  sigardiv  47305  sigarcol  47308  sharhght  47309  sigaradd  47310  cevathlem1  47311  cevathlem2  47312  cevath  47313  proththd  48093  perfectALTVlem2  48214  gpgnbgrvtx0  48566  gpgnbgrvtx1  48567  imasubc2  49643  imaf1co  49646  idfullsubc  49652  fucofulem1  49801