Theorem simp2d 1139

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp2bi  1142  f1dom3fv3dif  7026  f1dom3el3dif  7027  f1prex  7040  oeeui  8228  resixp  8497  domssex  8678  cantnflem1a  9148  cantnflem1d  9151  cantnflem3  9154  cantnflem4  9155  fpwwe2lem7  10058  canthnumlem  10070  canthp1lem2  10075  wun0  10140  lelttrdi  10802  supmullem2  11612  supmul  11613  ixxdisj  12754  ixxun  12755  ixxss1  12757  ixxss2  12758  ixxss12  12759  ixxub  12760  ixxlb  12761  ubioo  12771  elicore  12790  iccgelb  12794  iccss2  12808  icodisj  12863  xov1plusxeqvd  12885  fldiv  13229  immul  14495  sqrtge0  14617  sqrtrege0  14725  icco1  14897  ruclem2  15585  ruclem3  15586  ruclem8  15590  ruclem12  15594  gcddvds  15852  crth  16115  phimullem  16116  eulerthlem1  16118  eulerthlem2  16119  prmreclem3  16254  sectcan  17025  sectco  17026  sectmon  17052  monsect  17053  funcixp  17137  funcsect  17142  invfuc  17244  coapm  17331  catciso  17367  posasymb  17562  ipodrsima  17775  pstr2  17815  psdmrn  17817  psref  17818  mhmlin  17963  subm0cl  17976  eqger  18330  eqgcpbl  18334  gaorber  18438  orbstafun  18441  cayleyth  18543  pmtrrn2  18588  pmtrfinv  18589  dfod2  18691  sylow2blem1  18745  dprdf  19128  dprdff  19134  dprdfcl  19135  dprdsplit  19170  dpjcntz  19174  ablfac1a  19191  ablfac1b  19192  lmodvsdi  19657  lbssp  19851  2idlcpbl  20007  assaring  20093  mpff  20317  mpfaddcl  20318  mpfmulcl  20319  mpfind  20320  pf1rcl  20512  mpfpf1  20514  mdetunilem2  21222  mdetunilem5  21225  mdetunilem6  21226  chfacfisfcpmat  21463  pnfnei  21828  cnptop2  21851  lmcl  21905  lmcnp  21912  flimfil  22577  tlmlmod  22797  ustbasel  22815  ustincl  22816  ustinvel  22818  ustfilxp  22821  tusunif  22878  imasdsf1olem  22983  xmeter  23043  tmsds  23094  metustexhalf  23166  nlmlmod  23287  qdensere  23378  blcvx  23406  tgqioo  23408  icccmplem2  23431  reconnlem1  23434  cnmpopc  23532  phtpcer  23599  phtpcco2  23603  pcohtpylem  23623  pcohtpy  23624  pcophtb  23633  om1addcl  23637  pi1blem  23643  pi1cpbl  23648  pi1grplem  23653  pi1inv  23656  pi1xfrf  23657  pi1xfr  23659  pi1xfrcnvlem  23660  pi1cof  23663  pi1coghm  23665  cphnlm  23776  cphsqrtcl2  23790  tcphcph  23840  lmcau  23916  bcthlem4  23930  minveclem4c  24028  minveclem2  24029  minveclem3b  24031  minveclem4  24035  minveclem6  24037  ivthicc  24059  ovolfsval  24071  ovollb2lem  24089  ovolshftlem1  24110  ovolscalem1  24114  ovolicc1  24117  ovolicc2lem2  24119  ovolicc2lem4  24121  ovolicc2lem5  24122  ovolicopnf  24125  ioombl1lem1  24159  ioombl1lem3  24161  ioombl1lem4  24162  uniioovol  24180  uniioombllem2a  24183  uniioombllem2  24184  uniioombllem3a  24185  uniioombllem3  24186  uniioombllem4  24187  uniioombllem6  24189  dyadmaxlem  24198  volivth  24208  vitalilem2  24210  vitalilem5  24213  i1frn  24278  itg2monolem1  24351  itgcnlem  24390  itgrevallem1  24395  itgreval  24397  itgle  24410  ibladd  24421  iblabslem  24428  itgspliticc  24437  itgsplitioo  24438  ditgcl  24456  ditgswap  24457  ditgsplitlem  24458  limcdif  24474  limcresi  24483  limccnp  24489  limccnp2  24490  limcco  24491  dvlip  24590  dvlip2  24592  dveq0  24597  dvgt0lem1  24599  dvivthlem1  24605  dvcnvrelem1  24614  dvcnvre  24616  dvfsumlem2  24624  ftc1lem1  24632  ftc1a  24634  ftc1lem4  24636  ftc2ditglem  24642  itgsubstlem  24645  ply1rem  24757  fta1glem1  24759  ig1pdvds  24770  plyrem  24894  facth  24895  fta1lem  24896  vieta1lem1  24899  vieta1lem2  24900  aaliou3lem3  24933  aaliou3lem4  24935  aaliou3lem7  24938  taylfvallem1  24945  tayl0  24950  taylply2  24956  radcnvle  25008  psercnlem2  25012  psercnlem1  25013  psercn  25014  pserdvlem1  25015  pserdvlem2  25016  abelth2  25030  coseq00topi  25088  coseq0negpitopi  25089  cosordlem  25115  tanord1  25121  efif1olem1  25126  loglesqrt  25339  logreclem  25340  relogbval  25350  nnlogbexp  25359  chordthmlem4  25413  quart1  25434  quartlem2  25436  quartlem3  25437  quartlem4  25438  quart  25439  acosbnd  25478  atancj  25488  atanlogsublem  25493  atantan  25501  atanbndlem  25503  dvatan  25513  atantayl  25515  rlimcnp2  25544  divsqrtsumlem  25557  ftalem5  25654  ftalem7  25656  basellem4  25661  basellem5  25662  perfectlem2  25806  dchrinv  25837  chpdifbndlem1  26129  pntibndlem2  26167  pntlemc  26171  pntlema  26172  pntlemb  26173  pntlemg  26174  pntlemh  26175  pntlemq  26177  pntlemr  26178  pntlemj  26179  pntlemi  26180  pntlemf  26181  pntlemk  26182  pntlemo  26183  pntleme  26184  pntlem3  26185  pntleml  26187  abvcxp  26191  axtgpasch  26253  cgr3simp2  26307  legso  26385  hlne2  26392  hlln  26393  mirhl  26465  inagswap  26627  inagne2  26629  dfcgrg2  26649  subumgredg2  27067  upgrres1  27095  nb3grprlem1  27162  wlkp  27398  wspthsswwlkn  27697  2wlkdlem6  27710  clwwisshclwwsn  27794  erclwwlkeqlen  27797  erclwwlksym  27799  erclwwlktr  27800  clwwlkn  27804  clwwlknwrd  27812  clwwlknonex2e  27889  grpoass  28280  vcsm  28339  nvf  28437  ssps  28507  minvecolem2  28652  minvecolem4c  28656  minvecolem4  28657  minvecolem5  28658  minvecolem6  28659  eigvec1  29739  eliccelico  30500  elicoelioo  30501  pmtrto1cl  30741  cyc3evpm  30792  slmdvsdi  30843  slmdvs1  30848  imaslmod  30922  prmidlnr  30956  qsidomlem2  30966  mxidlnr  30973  cnre2csqlem  31153  lmxrge0  31195  sigaclci  31391  difelsiga  31392  insiga  31396  ldsysgenld  31419  sigapildsyslem  31420  sigapildsys  31421  ldgenpisyslem1  31422  measvnul  31465  sibfrn  31595  eulerpartlemt  31629  eulerpartlemmf  31633  tg5segofs  31944  lpadleft  31954  spthcycl  32376  subgrwlk  32379  acycgrcycl  32394  subfacp1lem2a  32427  subfacp1lem3  32429  subfacp1lem4  32430  subfacp1lem5  32431  sconnpht2  32485  sconnpi1  32486  resconn  32493  cvmsss  32514  cvmsn0  32515  cvmlift2lem3  32552  cvmlift2lem7  32556  cvmliftphtlem  32564  cvmliftpht  32565  cvmlift3lem5  32570  cvmlift3lem6  32571  msrf  32789  elmsta  32795  mclsax  32816  mthmpps  32829  mclspps  32831  scutun12  33271  slerec  33277  ivthALT  33683  poimirlem17  34924  poimirlem20  34927  ibladdnc  34964  iblabsnclem  34970  ftc1cnnclem  34980  ftc1anc  34990  ftc2nc  34991  heiborlem3  35106  iccbnd  35133  rngohom1  35261  idl0cl  35311  maxidlnr  35335  lshpne  36133  opococ  36346  opexmid  36358  hlclat  36509  lclkrslem2  38689  gneispacern2  40538  cvgdvgrat  40694  iccshift  41843  iccsuble  41844  icoiccdif  41849  mullimc  41946  limccog  41950  mullimcf  41953  lptioo2  41961  limcmptdm  41965  limcicciooub  41967  xlimmnfvlem1  42162  xlimpnfvlem1  42166  icccncfext  42219  cncfioobdlem  42228  ditgeqiooicc  42294  itgsubsticc  42310  iblcncfioo  42312  itgiccshift  42314  itgperiod  42315  itgsbtaddcnst  42316  stoweidlem11  42345  stoweidlem31  42365  stoweidlem36  42370  stoweidlem38  42372  stoweidlem44  42378  stoweidlem62  42396  dirkercncflem1  42437  dirkercncflem4  42440  fourierdlem26  42467  fourierdlem32  42473  fourierdlem33  42474  fourierdlem37  42478  fourierdlem42  42483  fourierdlem54  42494  fourierdlem63  42503  fourierdlem64  42504  fourierdlem65  42505  fourierdlem69  42509  fourierdlem74  42514  fourierdlem75  42515  fourierdlem79  42519  fourierdlem81  42521  fourierdlem82  42522  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem93  42533  fourierdlem101  42541  fourierdlem111  42551  saldifcl  42653  unisalgen2  42686  hoidmv1lelem3  42924  smff  43058  smfpimltxr  43073  sigardiv  43167  sigarcol  43170  sharhght  43171  sigaradd  43172  cevathlem1  43173  cevathlem2  43174  cevath  43175  proththd  43828  perfectALTVlem2  43936