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  7272  f1dom3el3dif  7273  f1prex  7292  oeeui  8614  resixp  8964  domssex  9160  cantnflem1a  9689  cantnflem1d  9692  cantnflem3  9695  cantnflem4  9696  fpwwe2lem6  10724  canthnumlem  10736  canthp1lem2  10741  wun0  10806  lelttrdi  11475  supmullem2  12291  supmul  12292  ixxdisj  13494  ixxun  13495  ixxss1  13497  ixxss2  13498  ixxss12  13499  ixxub  13500  ixxlb  13501  ubioo  13511  elicore  13532  iccgelb  13536  iccss2  13551  icodisj  13610  xov1plusxeqvd  13632  fldiv  14003  immul  15308  sqrtge0  15429  sqrtrege0  15538  icco1  15712  ruclem2  16405  ruclem3  16406  ruclem8  16410  ruclem12  16414  gcddvds  16678  crth  16960  phimullem  16961  eulerthlem1  16963  eulerthlem2  16964  prmreclem3  17101  sectcan  17935  sectco  17936  sectmon  17962  monsect  17963  funcixp  18047  funcsect  18052  invfuc  18157  coapm  18251  catciso  18291  posasymb  18498  ipodrsima  18720  pstr2  18750  psdmrn  18752  psref  18753  mhmlin  18993  subm0cl  19011  eqger  19395  eqgcpbl  19399  gaorber  19527  orbstafun  19530  cayleyth  19634  pmtrrn2  19679  pmtrfinv  19680  dfod2  19783  sylow2blem1  19839  dprdf  20227  dprdff  20233  dprdfcl  20234  dprdsplit  20269  dpjcntz  20273  ablfac1a  20290  ablfac1b  20291  lmodvsdi  21165  lbssp  21359  2idlcpblrng  21570  prmidlnr  21625  qsidomlem2  21642  evlsval3  22403  mpff  22426  mpfaddcl  22427  mpfmulcl  22428  mpfind  22429  pf1rcl  22672  mpfpf1  22674  mdetunilem2  22933  mdetunilem5  22936  mdetunilem6  22937  chfacfisfcpmat  23178  pnfnei  23543  cnptop2  23566  lmcl  23620  lmcnp  23627  flimfil  24293  tlmlmod  24513  ustbasel  24531  ustincl  24532  ustinvel  24534  ustfilxp  24537  tusunif  24592  imasdsf1olem  24697  xmeter  24757  tmsds  24808  metustexhalf  24880  nlmlmod  25002  qdensere  25093  blcvx  25122  tgqioo  25124  icccmplem2  25148  reconnlem1  25151  cnmpopc  25254  phtpcer  25321  phtpcco2  25325  pcohtpylem  25345  pcohtpy  25346  pcophtb  25355  om1addcl  25359  pi1blem  25365  pi1cpbl  25370  pi1grplem  25375  pi1inv  25378  pi1xfrf  25379  pi1xfr  25381  pi1xfrcnvlem  25382  pi1cof  25385  pi1coghm  25387  cphnlm  25498  cphsqrtcl2  25512  tcphcph  25563  lmcau  25639  bcthlem4  25653  minveclem4c  25751  minveclem2  25752  minveclem3b  25754  minveclem4  25758  minveclem6  25760  ivthicc  25784  ovolfsval  25796  ovollb2lem  25814  ovolshftlem1  25835  ovolscalem1  25839  ovolicc1  25842  ovolicc2lem2  25844  ovolicc2lem4  25846  ovolicc2lem5  25847  ovolicopnf  25850  ioombl1lem1  25884  ioombl1lem3  25886  ioombl1lem4  25887  uniioovol  25905  uniioombllem2a  25908  uniioombllem2  25909  uniioombllem3a  25910  uniioombllem3  25911  uniioombllem4  25912  uniioombllem6  25914  dyadmaxlem  25923  volivth  25933  vitalilem2  25935  vitalilem5  25938  i1frn  26003  itg2monolem1  26076  itgcnlem  26115  itgrevallem1  26120  itgreval  26122  itgle  26135  ibladd  26146  iblabslem  26153  itgspliticc  26162  itgsplitioo  26163  ditgcl  26183  ditgswap  26184  ditgsplitlem  26185  limcdif  26201  limcresi  26210  limccnp  26216  limccnp2  26217  limcco  26218  dvlip  26318  dvlip2  26320  dveq0  26325  dvgt0lem1  26327  dvivthlem1  26333  dvcnvrelem1  26342  dvcnvre  26344  dvfsumlem2  26352  ftc1lem1  26360  ftc1a  26362  ftc1lem4  26364  ftc2ditglem  26370  itgsubstlem  26373  ply1rem  26489  fta1glem1  26491  ig1pdvds  26503  plyrem  26631  facth  26632  fta1lem  26633  vieta1lem1  26638  vieta1lem2  26639  aaliou3lem3  26676  aaliou3lem4  26678  aaliou3lem7  26681  taylfvallem1  26689  tayl0  26694  taylply2  26700  radcnvle  26752  psercnlem2  26756  psercnlem1  26757  psercn  26758  pserdvlem1  26759  pserdvlem2  26760  abelth2  26774  coseq00topi  26836  coseq0negpitopi  26837  cosordlem  26863  tanord1  26870  efif1olem1  26875  loglesqrt  27094  logreclem  27095  relogbval  27105  nnlogbexp  27114  chordthmlem4  27168  quart1  27189  quartlem2  27191  quartlem3  27192  quartlem4  27193  quart  27194  acosbnd  27233  atancj  27243  atanlogsublem  27248  atantan  27256  atanbndlem  27258  dvatan  27268  atantayl  27270  rlimcnp2  27299  divsqrtsumlem  27312  ftalem5  27409  ftalem7  27411  basellem4  27416  basellem5  27417  perfectlem2  27562  dchrinv  27593  chpdifbndlem1  27885  pntibndlem2  27923  pntlemc  27927  pntlema  27928  pntlemb  27929  pntlemg  27930  pntlemh  27931  pntlemq  27933  pntlemr  27934  pntlemj  27935  pntlemi  27936  pntlemf  27937  pntlemk  27938  pntlemo  27939  pntleme  27940  pntlem3  27941  pntleml  27943  abvcxp  27947  flt4lem5f  27992  flt4lem7  27994  nna4b4nsq  27995  cutsun12  28181  lesrec  28190  eqcuts3  28195  cofcut2  28313  cofcutr  28315  cofcutrtime  28318  cutmax  28325  cutmin  28326  addsproplem4  28363  addsproplem6  28365  addsuniflem  28392  addsasslem1  28394  addsasslem2  28395  negsproplem5  28423  negsproplem6  28424  negcut2  28431  negsunif  28446  mulsproplem12  28518  sltmuls1  28538  sltmuls2  28539  mulsuniflem  28540  precsexlem11  28608  twocut  28814  pw2cut2  28853  axtgpasch  28934  cgr3simp2  28989  legso  29067  hlne2  29077  hlln  29078  mirhl  29156  inagswap  29365  inagne2  29367  dfcgrg2  29413  subumgredg2  29871  upgrres1  29899  nb3grprlem1  29966  wlkp  30202  subgrwlk  30274  spthcycl  30397  wspthsswwlkn  30512  2wlkdlem6  30525  clwwisshclwwsn  30612  erclwwlkeqlen  30615  erclwwlksym  30617  erclwwlktr  30618  clwwlkn  30622  clwwlknwrd  30630  clwwlknonex2e  30706  acycgrcycl  30758  grpoass  31110  vcsm  31169  nvf  31267  ssps  31337  minvecolem2  31482  minvecolem4c  31486  minvecolem4  31487  minvecolem5  31488  minvecolem6  31489  eigvec1  32569  inagbtwn  33053  cgrgptxfr  33058  inagcgratrgncol  33062  tgaasne  33087  eliccelico  33415  elicoelioo  33416  pmtrto1cl  33706  cyc3evpm  33757  slmdvsdi  33822  slmdvs1  33827  sdrgdvcl  33907  sdrginvcl  33908  fldgenssp  33926  imaslmod  33960  mxidlnr  34035  0ringmon1p  34135  irngnzply1lem  34368  irngnzply1  34369  ply1annig1p  34382  minplycl  34384  ply1annprmidl  34385  minplym1p  34391  minplynzm1p  34392  algextdeglem1  34395  algextdeglem2  34396  algextdeglem3  34397  algextdeglem4  34398  algextdeglem5  34399  constrsqrtcl  34457  cnre2csqlem  34588  lmxrge0  34630  sigaclci  34810  difunielsiga  34811  insiga  34816  ldsysgenld  34839  sigapildsyslem  34840  sigapildsys  34841  ldgenpisyslem1  34842  measvnul  34885  sibfrn  35015  eulerpartlemt  35049  eulerpartlemmf  35053  tg5segofs  35351  lpadleft  35361  subfacp1lem2a  36031  subfacp1lem3  36033  subfacp1lem4  36034  subfacp1lem5  36035  sconnpht2  36089  sconnpi1  36090  resconn  36097  cvmsss  36118  cvmsn0  36119  cvmlift2lem3  36156  cvmlift2lem7  36160  cvmliftphtlem  36168  cvmliftpht  36169  cvmlift3lem5  36174  cvmlift3lem6  36175  msrf  36393  elmsta  36399  mclsax  36420  mthmpps  36433  mclspps  36435  ivthALT  37215  weiunpo  37345  weiunso  37346  weiunfr  37347  weiunse  37348  poimirlem17  38648  poimirlem20  38651  ibladdnc  38688  iblabsnclem  38694  ftc1cnnclem  38702  ftc1anc  38712  ftc2nc  38713  heiborlem3  38840  iccbnd  38867  rngohom1  38995  idl0cl  39045  maxidlnr  39069  lshpne  40132  opococ  40345  opexmid  40357  hlclat  40508  lclkrslem2  42688  fzne2d  43123  dvrelog2  43207  dvrelog3  43208  0nonelalab  43210  aks4d1p1p5  43218  primrootsunit1  43240  primrootscoprmpow  43242  primrootscoprbij  43245  primrootspoweq0  43249  aks6d1c2lem3  43269  aks6d1c2  43273  aks6d1c6lem5  43320  aks5lem1  43329  aks5lem2  43330  aks5lem3a  43332  aks5lem5a  43334  unitscyglem1  43338  gneispacern2  45232  cvgdvgrat  45390  iccshift  46623  iccsuble  46624  icoiccdif  46629  mullimc  46721  limccog  46725  mullimcf  46728  lptioo2  46736  limcmptdm  46738  limcicciooub  46740  xlimmnfvlem1  46935  xlimpnfvlem1  46939  icccncfext  46990  cncfioobdlem  46999  ditgeqiooicc  47063  itgsubsticc  47079  iblcncfioo  47081  itgiccshift  47083  itgperiod  47084  itgsbtaddcnst  47085  stoweidlem31  47134  stoweidlem36  47139  stoweidlem38  47141  stoweidlem44  47147  stoweidlem62  47165  dirkercncflem1  47206  dirkercncflem4  47209  fourierdlem26  47236  fourierdlem32  47242  fourierdlem33  47243  fourierdlem37  47247  fourierdlem42  47252  fourierdlem54  47263  fourierdlem63  47272  fourierdlem64  47273  fourierdlem65  47274  fourierdlem69  47278  fourierdlem74  47283  fourierdlem75  47284  fourierdlem79  47288  fourierdlem81  47290  fourierdlem82  47291  fourierdlem89  47298  fourierdlem90  47299  fourierdlem91  47300  fourierdlem93  47302  fourierdlem101  47310  fourierdlem111  47320  saldifcl  47422  unisalgen2  47457  hoidmv1lelem3  47696  smff  47835  sigardiv  47964  sigarcol  47967  sharhght  47968  sigaradd  47969  cevathlem1  47970  cevathlem2  47971  cevath  47972  proththd  48792  perfectALTVlem2  48913  gpgnbgrvtx0  49265  gpgnbgrvtx1  49266  imasubc2  50361  imaf1co  50364  idfullsubc  50370  fucofulem1  50525  parcatid2  50856  parcatid  50857  rr3fv2cld  51116