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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simp2bi  1145  f1dom3fv3dif  7150  f1dom3el3dif  7151  f1prex  7165  oeeui  8442  resixp  8730  domssex  8934  cantnflem1a  9452  cantnflem1d  9455  cantnflem3  9458  cantnflem4  9459  fpwwe2lem6  10401  canthnumlem  10413  canthp1lem2  10418  wun0  10483  lelttrdi  11146  supmullem2  11955  supmul  11956  ixxdisj  13103  ixxun  13104  ixxss1  13106  ixxss2  13107  ixxss12  13108  ixxub  13109  ixxlb  13110  ubioo  13120  elicore  13140  iccgelb  13144  iccss2  13159  icodisj  13217  xov1plusxeqvd  13239  fldiv  13589  immul  14856  sqrtge0  14978  sqrtrege0  15086  icco1  15258  ruclem2  15950  ruclem3  15951  ruclem8  15955  ruclem12  15959  gcddvds  16219  crth  16488  phimullem  16489  eulerthlem1  16491  eulerthlem2  16492  prmreclem3  16628  sectcan  17476  sectco  17477  sectmon  17503  monsect  17504  funcixp  17591  funcsect  17596  invfuc  17701  coapm  17795  catciso  17835  posasymb  18046  ipodrsima  18268  pstr2  18298  psdmrn  18300  psref  18301  mhmlin  18446  subm0cl  18459  eqger  18815  eqgcpbl  18819  gaorber  18923  orbstafun  18926  cayleyth  19032  pmtrrn2  19077  pmtrfinv  19078  dfod2  19180  sylow2blem1  19234  dprdf  19618  dprdff  19624  dprdfcl  19625  dprdsplit  19660  dpjcntz  19664  ablfac1a  19681  ablfac1b  19682  lmodvsdi  20155  lbssp  20350  2idlcpbl  20514  assaring  21077  mpff  21323  mpfaddcl  21324  mpfmulcl  21325  mpfind  21326  pf1rcl  21524  mpfpf1  21526  mdetunilem2  21771  mdetunilem5  21774  mdetunilem6  21775  chfacfisfcpmat  22013  pnfnei  22380  cnptop2  22403  lmcl  22457  lmcnp  22464  flimfil  23129  tlmlmod  23349  ustbasel  23367  ustincl  23368  ustinvel  23370  ustfilxp  23373  tusunif  23430  imasdsf1olem  23535  xmeter  23595  tmsds  23649  metustexhalf  23721  nlmlmod  23851  qdensere  23942  blcvx  23970  tgqioo  23972  icccmplem2  23995  reconnlem1  23998  cnmpopc  24100  phtpcer  24167  phtpcco2  24171  pcohtpylem  24191  pcohtpy  24192  pcophtb  24201  om1addcl  24205  pi1blem  24211  pi1cpbl  24216  pi1grplem  24221  pi1inv  24224  pi1xfrf  24225  pi1xfr  24227  pi1xfrcnvlem  24228  pi1cof  24231  pi1coghm  24233  cphnlm  24345  cphsqrtcl2  24359  tcphcph  24410  lmcau  24486  bcthlem4  24500  minveclem4c  24598  minveclem2  24599  minveclem3b  24601  minveclem4  24605  minveclem6  24607  ivthicc  24631  ovolfsval  24643  ovollb2lem  24661  ovolshftlem1  24682  ovolscalem1  24686  ovolicc1  24689  ovolicc2lem2  24691  ovolicc2lem4  24693  ovolicc2lem5  24694  ovolicopnf  24697  ioombl1lem1  24731  ioombl1lem3  24733  ioombl1lem4  24734  uniioovol  24752  uniioombllem2a  24755  uniioombllem2  24756  uniioombllem3a  24757  uniioombllem3  24758  uniioombllem4  24759  uniioombllem6  24761  dyadmaxlem  24770  volivth  24780  vitalilem2  24782  vitalilem5  24785  i1frn  24850  itg2monolem1  24924  itgcnlem  24963  itgrevallem1  24968  itgreval  24970  itgle  24983  ibladd  24994  iblabslem  25001  itgspliticc  25010  itgsplitioo  25011  ditgcl  25031  ditgswap  25032  ditgsplitlem  25033  limcdif  25049  limcresi  25058  limccnp  25064  limccnp2  25065  limcco  25066  dvlip  25166  dvlip2  25168  dveq0  25173  dvgt0lem1  25175  dvivthlem1  25181  dvcnvrelem1  25190  dvcnvre  25192  dvfsumlem2  25200  ftc1lem1  25208  ftc1a  25210  ftc1lem4  25212  ftc2ditglem  25218  itgsubstlem  25221  ply1rem  25337  fta1glem1  25339  ig1pdvds  25350  plyrem  25474  facth  25475  fta1lem  25476  vieta1lem1  25479  vieta1lem2  25480  aaliou3lem3  25513  aaliou3lem4  25515  aaliou3lem7  25518  taylfvallem1  25525  tayl0  25530  taylply2  25536  radcnvle  25588  psercnlem2  25592  psercnlem1  25593  psercn  25594  pserdvlem1  25595  pserdvlem2  25596  abelth2  25610  coseq00topi  25668  coseq0negpitopi  25669  cosordlem  25695  tanord1  25702  efif1olem1  25707  loglesqrt  25920  logreclem  25921  relogbval  25931  nnlogbexp  25940  chordthmlem4  25994  quart1  26015  quartlem2  26017  quartlem3  26018  quartlem4  26019  quart  26020  acosbnd  26059  atancj  26069  atanlogsublem  26074  atantan  26082  atanbndlem  26084  dvatan  26094  atantayl  26096  rlimcnp2  26125  divsqrtsumlem  26138  ftalem5  26235  ftalem7  26237  basellem4  26242  basellem5  26243  perfectlem2  26387  dchrinv  26418  chpdifbndlem1  26710  pntibndlem2  26748  pntlemc  26752  pntlema  26753  pntlemb  26754  pntlemg  26755  pntlemh  26756  pntlemq  26758  pntlemr  26759  pntlemj  26760  pntlemi  26761  pntlemf  26762  pntlemk  26763  pntlemo  26764  pntleme  26765  pntlem3  26766  pntleml  26768  abvcxp  26772  axtgpasch  26837  cgr3simp2  26891  legso  26969  hlne2  26976  hlln  26977  mirhl  27049  inagswap  27211  inagne2  27213  dfcgrg2  27233  subumgredg2  27661  upgrres1  27689  nb3grprlem1  27756  wlkp  27992  wspthsswwlkn  28292  2wlkdlem6  28305  clwwisshclwwsn  28389  erclwwlkeqlen  28392  erclwwlksym  28394  erclwwlktr  28395  clwwlkn  28399  clwwlknwrd  28407  clwwlknonex2e  28483  grpoass  28874  vcsm  28933  nvf  29031  ssps  29101  minvecolem2  29246  minvecolem4c  29250  minvecolem4  29251  minvecolem5  29252  minvecolem6  29253  eigvec1  30333  eliccelico  31107  elicoelioo  31108  pmtrto1cl  31375  cyc3evpm  31426  slmdvsdi  31477  slmdvs1  31482  imaslmod  31562  prmidlnr  31623  qsidomlem2  31638  mxidlnr  31645  cnre2csqlem  31869  lmxrge0  31911  sigaclci  32109  difelsiga  32110  insiga  32114  ldsysgenld  32137  sigapildsyslem  32138  sigapildsys  32139  ldgenpisyslem1  32140  measvnul  32183  sibfrn  32313  eulerpartlemt  32347  eulerpartlemmf  32351  tg5segofs  32662  lpadleft  32672  spthcycl  33100  subgrwlk  33103  acycgrcycl  33118  subfacp1lem2a  33151  subfacp1lem3  33153  subfacp1lem4  33154  subfacp1lem5  33155  sconnpht2  33209  sconnpi1  33210  resconn  33217  cvmsss  33238  cvmsn0  33239  cvmlift2lem3  33276  cvmlift2lem7  33280  cvmliftphtlem  33288  cvmliftpht  33289  cvmlift3lem5  33294  cvmlift3lem6  33295  msrf  33513  elmsta  33519  mclsax  33540  mthmpps  33553  mclspps  33555  scutun12  34013  slerec  34022  cofcut2  34100  cofcutr  34101  cofcutrtime  34102  ivthALT  34533  poimirlem17  35803  poimirlem20  35806  ibladdnc  35843  iblabsnclem  35849  ftc1cnnclem  35857  ftc1anc  35867  ftc2nc  35868  heiborlem3  35980  iccbnd  36007  rngohom1  36135  idl0cl  36185  maxidlnr  36209  lshpne  37003  opococ  37216  opexmid  37228  hlclat  37379  lclkrslem2  39559  fzne2d  39996  dvrelog2  40079  dvrelog3  40080  0nonelalab  40082  aks4d1p1p5  40090  metakunt8  40139  metakunt21  40152  metakunt22  40153  metakunt24  40155  metakunt25  40156  evlsval3  40279  flt4lem5f  40501  flt4lem7  40503  nna4b4nsq  40504  gneispacern2  41756  cvgdvgrat  41938  iccshift  43063  iccsuble  43064  icoiccdif  43069  mullimc  43164  limccog  43168  mullimcf  43171  lptioo2  43179  limcmptdm  43183  limcicciooub  43185  xlimmnfvlem1  43380  xlimpnfvlem1  43384  icccncfext  43435  cncfioobdlem  43444  ditgeqiooicc  43508  itgsubsticc  43524  iblcncfioo  43526  itgiccshift  43528  itgperiod  43529  itgsbtaddcnst  43530  stoweidlem31  43579  stoweidlem36  43584  stoweidlem38  43586  stoweidlem44  43592  stoweidlem62  43610  dirkercncflem1  43651  dirkercncflem4  43654  fourierdlem26  43681  fourierdlem32  43687  fourierdlem33  43688  fourierdlem37  43692  fourierdlem42  43697  fourierdlem54  43708  fourierdlem63  43717  fourierdlem64  43718  fourierdlem65  43719  fourierdlem69  43723  fourierdlem74  43728  fourierdlem75  43729  fourierdlem79  43733  fourierdlem81  43735  fourierdlem82  43736  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem93  43747  fourierdlem101  43755  fourierdlem111  43765  saldifcl  43867  unisalgen2  43900  hoidmv1lelem3  44138  smff  44277  sigardiv  44388  sigarcol  44391  sharhght  44392  sigaradd  44393  cevathlem1  44394  cevathlem2  44395  cevath  44396  proththd  45077  perfectALTVlem2  45185