Theorem simp2d 1142

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 1136	. 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  1145  f1dom3fv3dif  7287  f1dom3el3dif  7288  f1prex  7303  oeeui  8638  resixp  8971  domssex  9176  cantnflem1a  9722  cantnflem1d  9725  cantnflem3  9728  cantnflem4  9729  fpwwe2lem6  10673  canthnumlem  10685  canthp1lem2  10690  wun0  10755  lelttrdi  11420  supmullem2  12236  supmul  12237  ixxdisj  13398  ixxun  13399  ixxss1  13401  ixxss2  13402  ixxss12  13403  ixxub  13404  ixxlb  13405  ubioo  13415  elicore  13435  iccgelb  13439  iccss2  13454  icodisj  13512  xov1plusxeqvd  13534  fldiv  13896  immul  15171  sqrtge0  15292  sqrtrege0  15400  icco1  15572  ruclem2  16264  ruclem3  16265  ruclem8  16269  ruclem12  16273  gcddvds  16536  crth  16811  phimullem  16812  eulerthlem1  16814  eulerthlem2  16815  prmreclem3  16951  sectcan  17802  sectco  17803  sectmon  17829  monsect  17830  funcixp  17917  funcsect  17922  invfuc  18030  coapm  18124  catciso  18164  posasymb  18376  ipodrsima  18598  pstr2  18628  psdmrn  18630  psref  18631  mhmlin  18818  subm0cl  18836  eqger  19208  eqgcpbl  19212  gaorber  19338  orbstafun  19341  cayleyth  19447  pmtrrn2  19492  pmtrfinv  19493  dfod2  19596  sylow2blem1  19652  dprdf  20040  dprdff  20046  dprdfcl  20047  dprdsplit  20082  dpjcntz  20086  ablfac1a  20103  ablfac1b  20104  lmodvsdi  20899  lbssp  21095  2idlcpblrng  21298  mpff  22145  mpfaddcl  22146  mpfmulcl  22147  mpfind  22148  pf1rcl  22368  mpfpf1  22370  mdetunilem2  22634  mdetunilem5  22637  mdetunilem6  22638  chfacfisfcpmat  22876  pnfnei  23243  cnptop2  23266  lmcl  23320  lmcnp  23327  flimfil  23992  tlmlmod  24212  ustbasel  24230  ustincl  24231  ustinvel  24233  ustfilxp  24236  tusunif  24293  imasdsf1olem  24398  xmeter  24458  tmsds  24512  metustexhalf  24584  nlmlmod  24714  qdensere  24805  blcvx  24833  tgqioo  24835  icccmplem2  24858  reconnlem1  24861  cnmpopc  24968  phtpcer  25040  phtpcco2  25045  pcohtpylem  25065  pcohtpy  25066  pcophtb  25075  om1addcl  25079  pi1blem  25085  pi1cpbl  25090  pi1grplem  25095  pi1inv  25098  pi1xfrf  25099  pi1xfr  25101  pi1xfrcnvlem  25102  pi1cof  25105  pi1coghm  25107  cphnlm  25219  cphsqrtcl2  25233  tcphcph  25284  lmcau  25360  bcthlem4  25374  minveclem4c  25472  minveclem2  25473  minveclem3b  25475  minveclem4  25479  minveclem6  25481  ivthicc  25506  ovolfsval  25518  ovollb2lem  25536  ovolshftlem1  25557  ovolscalem1  25561  ovolicc1  25564  ovolicc2lem2  25566  ovolicc2lem4  25568  ovolicc2lem5  25569  ovolicopnf  25572  ioombl1lem1  25606  ioombl1lem3  25608  ioombl1lem4  25609  uniioovol  25627  uniioombllem2a  25630  uniioombllem2  25631  uniioombllem3a  25632  uniioombllem3  25633  uniioombllem4  25634  uniioombllem6  25636  dyadmaxlem  25645  volivth  25655  vitalilem2  25657  vitalilem5  25660  i1frn  25725  itg2monolem1  25799  itgcnlem  25839  itgrevallem1  25844  itgreval  25846  itgle  25859  ibladd  25870  iblabslem  25877  itgspliticc  25886  itgsplitioo  25887  ditgcl  25907  ditgswap  25908  ditgsplitlem  25909  limcdif  25925  limcresi  25934  limccnp  25940  limccnp2  25941  limcco  25942  dvlip  26046  dvlip2  26048  dveq0  26053  dvgt0lem1  26055  dvivthlem1  26061  dvcnvrelem1  26070  dvcnvre  26072  dvfsumlem2  26081  dvfsumlem2OLD  26082  ftc1lem1  26090  ftc1a  26092  ftc1lem4  26094  ftc2ditglem  26100  itgsubstlem  26103  ply1rem  26219  fta1glem1  26221  ig1pdvds  26233  plyrem  26361  facth  26362  fta1lem  26363  vieta1lem1  26366  vieta1lem2  26367  aaliou3lem3  26400  aaliou3lem4  26402  aaliou3lem7  26405  taylfvallem1  26412  tayl0  26417  taylply2  26423  taylply2OLD  26424  radcnvle  26477  psercnlem2  26482  psercnlem1  26483  psercn  26484  pserdvlem1  26485  pserdvlem2  26486  abelth2  26500  coseq00topi  26558  coseq0negpitopi  26559  cosordlem  26586  tanord1  26593  efif1olem1  26598  loglesqrt  26818  logreclem  26819  relogbval  26829  nnlogbexp  26838  chordthmlem4  26892  quart1  26913  quartlem2  26915  quartlem3  26916  quartlem4  26917  quart  26918  acosbnd  26957  atancj  26967  atanlogsublem  26972  atantan  26980  atanbndlem  26982  dvatan  26992  atantayl  26994  rlimcnp2  27023  divsqrtsumlem  27037  ftalem5  27134  ftalem7  27136  basellem4  27141  basellem5  27142  perfectlem2  27288  dchrinv  27319  chpdifbndlem1  27611  pntibndlem2  27649  pntlemc  27653  pntlema  27654  pntlemb  27655  pntlemg  27656  pntlemh  27657  pntlemq  27659  pntlemr  27660  pntlemj  27661  pntlemi  27662  pntlemf  27663  pntlemk  27664  pntlemo  27665  pntleme  27666  pntlem3  27667  pntleml  27669  abvcxp  27673  scutun12  27869  slerec  27878  cofcut2  27970  cofcutr  27972  cofcutrtime  27975  cutmax  27982  cutmin  27983  addsproplem4  28019  addsproplem6  28021  addsuniflem  28048  addsasslem1  28050  addsasslem2  28051  negsproplem5  28078  negsproplem6  28079  negscut2  28086  negsunif  28101  mulsproplem12  28167  ssltmul1  28187  ssltmul2  28188  mulsuniflem  28189  precsexlem11  28255  axtgpasch  28489  cgr3simp2  28543  legso  28621  hlne2  28628  hlln  28629  mirhl  28701  inagswap  28863  inagne2  28865  dfcgrg2  28885  subumgredg2  29316  upgrres1  29344  nb3grprlem1  29411  wlkp  29648  wspthsswwlkn  29947  2wlkdlem6  29960  clwwisshclwwsn  30044  erclwwlkeqlen  30047  erclwwlksym  30049  erclwwlktr  30050  clwwlkn  30054  clwwlknwrd  30062  clwwlknonex2e  30138  grpoass  30531  vcsm  30590  nvf  30688  ssps  30758  minvecolem2  30903  minvecolem4c  30907  minvecolem4  30908  minvecolem5  30909  minvecolem6  30910  eigvec1  31990  eliccelico  32785  elicoelioo  32786  pmtrto1cl  33101  cyc3evpm  33152  slmdvsdi  33203  slmdvs1  33208  sdrgdvcl  33280  sdrginvcl  33281  fldgenssp  33299  imaslmod  33360  prmidlnr  33446  qsidomlem2  33460  mxidlnr  33471  0ringmon1p  33562  irngnzply1lem  33704  irngnzply1  33705  ply1annig1p  33711  minplycl  33713  ply1annprmidl  33714  minplym1p  33720  algextdeglem1  33722  algextdeglem2  33723  algextdeglem3  33724  algextdeglem4  33725  algextdeglem5  33726  cnre2csqlem  33870  lmxrge0  33912  sigaclci  34112  difelsiga  34113  insiga  34117  ldsysgenld  34140  sigapildsyslem  34141  sigapildsys  34142  ldgenpisyslem1  34143  measvnul  34186  sibfrn  34318  eulerpartlemt  34352  eulerpartlemmf  34356  tg5segofs  34666  lpadleft  34676  spthcycl  35113  subgrwlk  35116  acycgrcycl  35131  subfacp1lem2a  35164  subfacp1lem3  35166  subfacp1lem4  35167  subfacp1lem5  35168  sconnpht2  35222  sconnpi1  35223  resconn  35230  cvmsss  35251  cvmsn0  35252  cvmlift2lem3  35289  cvmlift2lem7  35293  cvmliftphtlem  35301  cvmliftpht  35302  cvmlift3lem5  35307  cvmlift3lem6  35308  msrf  35526  elmsta  35532  mclsax  35553  mthmpps  35566  mclspps  35568  ivthALT  36317  weiunpo  36447  weiunso  36448  weiunfr  36449  weiunse  36450  poimirlem17  37623  poimirlem20  37626  ibladdnc  37663  iblabsnclem  37669  ftc1cnnclem  37677  ftc1anc  37687  ftc2nc  37688  heiborlem3  37799  iccbnd  37826  rngohom1  37954  idl0cl  38004  maxidlnr  38028  lshpne  38963  opococ  39176  opexmid  39188  hlclat  39339  lclkrslem2  41520  fzne2d  41961  dvrelog2  42045  dvrelog3  42046  0nonelalab  42048  aks4d1p1p5  42056  primrootsunit1  42078  primrootscoprmpow  42080  primrootscoprbij  42083  primrootspoweq0  42087  aks6d1c2lem3  42107  aks6d1c2  42111  aks6d1c6lem5  42158  aks5lem1  42167  aks5lem2  42168  aks5lem3a  42170  aks5lem5a  42172  unitscyglem1  42176  metakunt8  42193  metakunt21  42206  metakunt22  42207  metakunt24  42209  metakunt25  42210  evlsval3  42545  flt4lem5f  42643  flt4lem7  42645  nna4b4nsq  42646  gneispacern2  44128  cvgdvgrat  44308  iccshift  45470  iccsuble  45471  icoiccdif  45476  mullimc  45571  limccog  45575  mullimcf  45578  lptioo2  45586  limcmptdm  45590  limcicciooub  45592  xlimmnfvlem1  45787  xlimpnfvlem1  45791  icccncfext  45842  cncfioobdlem  45851  ditgeqiooicc  45915  itgsubsticc  45931  iblcncfioo  45933  itgiccshift  45935  itgperiod  45936  itgsbtaddcnst  45937  stoweidlem31  45986  stoweidlem36  45991  stoweidlem38  45993  stoweidlem44  45999  stoweidlem62  46017  dirkercncflem1  46058  dirkercncflem4  46061  fourierdlem26  46088  fourierdlem32  46094  fourierdlem33  46095  fourierdlem37  46099  fourierdlem42  46104  fourierdlem54  46115  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem69  46130  fourierdlem74  46135  fourierdlem75  46136  fourierdlem79  46140  fourierdlem81  46142  fourierdlem82  46143  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem93  46154  fourierdlem101  46162  fourierdlem111  46172  saldifcl  46274  unisalgen2  46309  hoidmv1lelem3  46548  smff  46687  sigardiv  46816  sigarcol  46819  sharhght  46820  sigaradd  46821  cevathlem1  46822  cevathlem2  46823  cevath  46824  proththd  47538  perfectALTVlem2  47646  gpgnbgrvtx0  47964  gpgnbgrvtx1  47965