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  7211  f1dom3el3dif  7212  f1prex  7227  oeeui  8526  resixp  8866  domssex  9061  cantnflem1a  9585  cantnflem1d  9588  cantnflem3  9591  cantnflem4  9592  fpwwe2lem6  10537  canthnumlem  10549  canthp1lem2  10554  wun0  10619  lelttrdi  11285  supmullem2  12103  supmul  12104  ixxdisj  13270  ixxun  13271  ixxss1  13273  ixxss2  13274  ixxss12  13275  ixxub  13276  ixxlb  13277  ubioo  13287  elicore  13308  iccgelb  13312  iccss2  13327  icodisj  13386  xov1plusxeqvd  13408  fldiv  13774  immul  15053  sqrtge0  15174  sqrtrege0  15283  icco1  15457  ruclem2  16151  ruclem3  16152  ruclem8  16156  ruclem12  16160  gcddvds  16424  crth  16699  phimullem  16700  eulerthlem1  16702  eulerthlem2  16703  prmreclem3  16840  sectcan  17672  sectco  17673  sectmon  17699  monsect  17700  funcixp  17784  funcsect  17789  invfuc  17894  coapm  17988  catciso  18028  posasymb  18235  ipodrsima  18457  pstr2  18487  psdmrn  18489  psref  18490  mhmlin  18711  subm0cl  18729  eqger  19100  eqgcpbl  19104  gaorber  19230  orbstafun  19233  cayleyth  19337  pmtrrn2  19382  pmtrfinv  19383  dfod2  19486  sylow2blem1  19542  dprdf  19930  dprdff  19936  dprdfcl  19937  dprdsplit  19972  dpjcntz  19976  ablfac1a  19993  ablfac1b  19994  lmodvsdi  20828  lbssp  21023  2idlcpblrng  21218  mpff  22049  mpfaddcl  22050  mpfmulcl  22051  mpfind  22052  pf1rcl  22274  mpfpf1  22276  mdetunilem2  22538  mdetunilem5  22541  mdetunilem6  22542  chfacfisfcpmat  22780  pnfnei  23145  cnptop2  23168  lmcl  23222  lmcnp  23229  flimfil  23894  tlmlmod  24114  ustbasel  24132  ustincl  24133  ustinvel  24135  ustfilxp  24138  tusunif  24193  imasdsf1olem  24298  xmeter  24358  tmsds  24409  metustexhalf  24481  nlmlmod  24603  qdensere  24694  blcvx  24723  tgqioo  24725  icccmplem2  24749  reconnlem1  24752  cnmpopc  24859  phtpcer  24931  phtpcco2  24936  pcohtpylem  24956  pcohtpy  24957  pcophtb  24966  om1addcl  24970  pi1blem  24976  pi1cpbl  24981  pi1grplem  24986  pi1inv  24989  pi1xfrf  24990  pi1xfr  24992  pi1xfrcnvlem  24993  pi1cof  24996  pi1coghm  24998  cphnlm  25109  cphsqrtcl2  25123  tcphcph  25174  lmcau  25250  bcthlem4  25264  minveclem4c  25362  minveclem2  25363  minveclem3b  25365  minveclem4  25369  minveclem6  25371  ivthicc  25396  ovolfsval  25408  ovollb2lem  25426  ovolshftlem1  25447  ovolscalem1  25451  ovolicc1  25454  ovolicc2lem2  25456  ovolicc2lem4  25458  ovolicc2lem5  25459  ovolicopnf  25462  ioombl1lem1  25496  ioombl1lem3  25498  ioombl1lem4  25499  uniioovol  25517  uniioombllem2a  25520  uniioombllem2  25521  uniioombllem3a  25522  uniioombllem3  25523  uniioombllem4  25524  uniioombllem6  25526  dyadmaxlem  25535  volivth  25545  vitalilem2  25547  vitalilem5  25550  i1frn  25615  itg2monolem1  25688  itgcnlem  25728  itgrevallem1  25733  itgreval  25735  itgle  25748  ibladd  25759  iblabslem  25766  itgspliticc  25775  itgsplitioo  25776  ditgcl  25796  ditgswap  25797  ditgsplitlem  25798  limcdif  25814  limcresi  25823  limccnp  25829  limccnp2  25830  limcco  25831  dvlip  25935  dvlip2  25937  dveq0  25942  dvgt0lem1  25944  dvivthlem1  25950  dvcnvrelem1  25959  dvcnvre  25961  dvfsumlem2  25970  dvfsumlem2OLD  25971  ftc1lem1  25979  ftc1a  25981  ftc1lem4  25983  ftc2ditglem  25989  itgsubstlem  25992  ply1rem  26108  fta1glem1  26110  ig1pdvds  26122  plyrem  26250  facth  26251  fta1lem  26252  vieta1lem1  26255  vieta1lem2  26256  aaliou3lem3  26289  aaliou3lem4  26291  aaliou3lem7  26294  taylfvallem1  26301  tayl0  26306  taylply2  26312  taylply2OLD  26313  radcnvle  26366  psercnlem2  26371  psercnlem1  26372  psercn  26373  pserdvlem1  26374  pserdvlem2  26375  abelth2  26389  coseq00topi  26448  coseq0negpitopi  26449  cosordlem  26476  tanord1  26483  efif1olem1  26488  loglesqrt  26708  logreclem  26709  relogbval  26719  nnlogbexp  26728  chordthmlem4  26782  quart1  26803  quartlem2  26805  quartlem3  26806  quartlem4  26807  quart  26808  acosbnd  26847  atancj  26857  atanlogsublem  26862  atantan  26870  atanbndlem  26872  dvatan  26882  atantayl  26884  rlimcnp2  26913  divsqrtsumlem  26927  ftalem5  27024  ftalem7  27026  basellem4  27031  basellem5  27032  perfectlem2  27178  dchrinv  27209  chpdifbndlem1  27501  pntibndlem2  27539  pntlemc  27543  pntlema  27544  pntlemb  27545  pntlemg  27546  pntlemh  27547  pntlemq  27549  pntlemr  27550  pntlemj  27551  pntlemi  27552  pntlemf  27553  pntlemk  27554  pntlemo  27555  pntleme  27556  pntlem3  27557  pntleml  27559  abvcxp  27563  scutun12  27761  slerec  27770  eqscut3  27775  cofcut2  27876  cofcutr  27878  cofcutrtime  27881  cutmax  27888  cutmin  27889  addsproplem4  27925  addsproplem6  27927  addsuniflem  27954  addsasslem1  27956  addsasslem2  27957  negsproplem5  27984  negsproplem6  27985  negscut2  27992  negsunif  28007  mulsproplem12  28076  ssltmul1  28096  ssltmul2  28097  mulsuniflem  28098  precsexlem11  28165  twocut  28356  pw2cut2  28392  axtgpasch  28455  cgr3simp2  28509  legso  28587  hlne2  28594  hlln  28595  mirhl  28667  inagswap  28829  inagne2  28831  dfcgrg2  28851  subumgredg2  29274  upgrres1  29302  nb3grprlem1  29369  wlkp  29606  wspthsswwlkn  29907  2wlkdlem6  29920  clwwisshclwwsn  30007  erclwwlkeqlen  30010  erclwwlksym  30012  erclwwlktr  30013  clwwlkn  30017  clwwlknwrd  30025  clwwlknonex2e  30101  grpoass  30494  vcsm  30553  nvf  30651  ssps  30721  minvecolem2  30866  minvecolem4c  30870  minvecolem4  30871  minvecolem5  30872  minvecolem6  30873  eigvec1  31953  eliccelico  32771  elicoelioo  32772  pmtrto1cl  33079  cyc3evpm  33130  slmdvsdi  33195  slmdvs1  33200  sdrgdvcl  33276  sdrginvcl  33277  fldgenssp  33295  imaslmod  33329  prmidlnr  33415  qsidomlem2  33429  mxidlnr  33440  0ringmon1p  33531  irngnzply1lem  33714  irngnzply1  33715  ply1annig1p  33728  minplycl  33730  ply1annprmidl  33731  minplym1p  33737  minplynzm1p  33738  algextdeglem1  33741  algextdeglem2  33742  algextdeglem3  33743  algextdeglem4  33744  algextdeglem5  33745  constrsqrtcl  33803  cnre2csqlem  33934  lmxrge0  33976  sigaclci  34156  difelsiga  34157  insiga  34161  ldsysgenld  34184  sigapildsyslem  34185  sigapildsys  34186  ldgenpisyslem1  34187  measvnul  34230  sibfrn  34361  eulerpartlemt  34395  eulerpartlemmf  34399  tg5segofs  34697  lpadleft  34707  spthcycl  35184  subgrwlk  35187  acycgrcycl  35202  subfacp1lem2a  35235  subfacp1lem3  35237  subfacp1lem4  35238  subfacp1lem5  35239  sconnpht2  35293  sconnpi1  35294  resconn  35301  cvmsss  35322  cvmsn0  35323  cvmlift2lem3  35360  cvmlift2lem7  35364  cvmliftphtlem  35372  cvmliftpht  35373  cvmlift3lem5  35378  cvmlift3lem6  35379  msrf  35597  elmsta  35603  mclsax  35624  mthmpps  35637  mclspps  35639  ivthALT  36390  weiunpo  36520  weiunso  36521  weiunfr  36522  weiunse  36523  poimirlem17  37687  poimirlem20  37690  ibladdnc  37727  iblabsnclem  37733  ftc1cnnclem  37741  ftc1anc  37751  ftc2nc  37752  heiborlem3  37863  iccbnd  37890  rngohom1  38018  idl0cl  38068  maxidlnr  38092  lshpne  39091  opococ  39304  opexmid  39316  hlclat  39467  lclkrslem2  41647  fzne2d  42083  dvrelog2  42167  dvrelog3  42168  0nonelalab  42170  aks4d1p1p5  42178  primrootsunit1  42200  primrootscoprmpow  42202  primrootscoprbij  42205  primrootspoweq0  42209  aks6d1c2lem3  42229  aks6d1c2  42233  aks6d1c6lem5  42280  aks5lem1  42289  aks5lem2  42290  aks5lem3a  42292  aks5lem5a  42294  unitscyglem1  42298  evlsval3  42667  flt4lem5f  42765  flt4lem7  42767  nna4b4nsq  42768  gneispacern2  44246  cvgdvgrat  44420  iccshift  45632  iccsuble  45633  icoiccdif  45638  mullimc  45730  limccog  45734  mullimcf  45737  lptioo2  45745  limcmptdm  45747  limcicciooub  45749  xlimmnfvlem1  45944  xlimpnfvlem1  45948  icccncfext  45999  cncfioobdlem  46008  ditgeqiooicc  46072  itgsubsticc  46088  iblcncfioo  46090  itgiccshift  46092  itgperiod  46093  itgsbtaddcnst  46094  stoweidlem31  46143  stoweidlem36  46148  stoweidlem38  46150  stoweidlem44  46156  stoweidlem62  46174  dirkercncflem1  46215  dirkercncflem4  46218  fourierdlem26  46245  fourierdlem32  46251  fourierdlem33  46252  fourierdlem37  46256  fourierdlem42  46261  fourierdlem54  46272  fourierdlem63  46281  fourierdlem64  46282  fourierdlem65  46283  fourierdlem69  46287  fourierdlem74  46292  fourierdlem75  46293  fourierdlem79  46297  fourierdlem81  46299  fourierdlem82  46300  fourierdlem89  46307  fourierdlem90  46308  fourierdlem91  46309  fourierdlem93  46311  fourierdlem101  46319  fourierdlem111  46329  saldifcl  46431  unisalgen2  46466  hoidmv1lelem3  46705  smff  46844  sigardiv  46973  sigarcol  46976  sharhght  46977  sigaradd  46978  cevathlem1  46979  cevathlem2  46980  cevath  46981  proththd  47728  perfectALTVlem2  47836  gpgnbgrvtx0  48188  gpgnbgrvtx1  48189  imasubc2  49267  imaf1co  49270  idfullsubc  49276  fucofulem1  49425