Theorem simp2bi 1146

Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
3simp1bi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp2bi	⊢ (𝜑 → 𝜒)

Proof of Theorem simp2bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
2	1	biimpi 216	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp2d 1143	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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:  0ellim  6375  smodm  8281  erdm  8642  ixpfn  8837  winafp  10610  inar1  10688  inatsk  10691  tskuni  10696  grur1  10733  supmullem1  12113  supmullem2  12114  supmul  12115  eluzelz  12763  elfz3nn0  13542  elfzo0l  13677  ico01fl0  13741  addmodlteq  13871  cshco  14761  swrds2  14865  ef01bndlem  16111  sin01bnd  16112  cos01bnd  16113  sin01gt0  16117  bitsss  16355  smueqlem  16419  gznegcl  16865  gzcjcl  16866  gzaddcl  16867  gzmulcl  16868  gzabssqcl  16871  4sqlem4a  16881  cshwshashlem2  17026  structn0fun  17080  xpsff1o  17489  mre1cl  17514  drsbn0  18228  subgss  19024  symgfixelsi  19332  psgnunilem5  19391  pgpgrp  19491  slwsubg  19507  efgs1b  19633  efgsp1  19634  efgsres  19635  efgredeu  19649  efgred2  19650  efgcpbllemb  19652  omndtos  20024  rngmgp  20059  srgmgp  20094  ringmgp  20142  irrednu  20328  sdrgsubrg  20694  fldsdrgfld  20701  sdrgint  20707  primefld  20708  primefld0cl  20709  primefld1cl  20710  orngogrp  20766  lmodring  20789  lmodprop2d  20845  lssn0  20861  phlsrng  21556  ocvss  21595  obsss  21649  locfinbas  23425  fclsfil  23913  tmdtps  23979  tgptmd  23982  trgring  24074  tdrgdrng  24077  ngpms  24504  icopnfcnv  24856  xrhmeo  24860  oprpiece1res2  24866  phtpcer  24910  pcoval2  24932  pcoass  24940  clmsca  24981  cphsqrtcl  25100  bncms  25260  itg2ge0  25652  uc1pn0  26067  mon1pn0  26068  sinq12ge0  26433  cosq14gt0  26435  cosq14ge0  26436  cos02pilt1  26451  cosq34lt1  26452  sinord  26459  recosf1o  26460  resinf1o  26461  logrnaddcl  26499  logbcl  26693  relogbreexp  26701  atanf  26806  atanneg  26833  atancj  26836  efiatan  26838  atanlogaddlem  26839  atanlogadd  26840  atanlogsub  26842  efiatan2  26843  2efiatan  26844  tanatan  26845  dvatan  26861  areambl  26884  rlimcnp  26891  emgt0  26933  harmoniclbnd  26935  harmonicbnd4  26937  lgamgulmlem2  26956  gausslemma2dlem1a  27292  2sqlem2  27345  2sqlem3  27347  dchrvmasumlem2  27425  dchrvmasumiflem1  27428  logdivbnd  27483  pntpbnd2  27514  pnt  27541  brbtwn2  28868  ax5seglem3  28894  ax5seglem6  28897  axpaschlem  28903  axcontlem2  28928  axcontlem4  28930  crctcshwlkn0lem4  29776  wwlkbp  29804  clwwisshclwwslem  29976  hst1a  32180  stge0  32186  sthil  32196  neldifpr1  32495  f1mptrn  32592  cshwrnid  32916  fsumrp0cl  32988  fzo0pmtrlast  33047  wrdpmtrlast  33048  psgnfzto1stlem  33055  slmdsrg  33159  primefldchr  33250  fldgensdrg  33263  primefldgen1  33270  1arithidomlem1  33482  1arithidomlem2  33483  1arithidom  33484  elunitge0  33865  xrge0iifcnv  33899  xrge0iifcv  33900  xrge0iifiso  33901  rrextnlm  33969  rrextchr  33970  0elros  34136  0elsros  34143  voliune  34195  volfiniune  34196  bnj563  34709  bnj1212  34765  bnj1219  34766  bnj1366  34795  bnj1379  34796  bnj545  34861  bnj594  34878  bnj1118  34950  bnj1177  34972  bnj1190  34974  bnj1398  35000  bnj1417  35007  bnj1450  35016  bnj1312  35024  bnj1523  35037  pthhashvtx  35100  msrval  35510  mclsppslem  35555  dfon2lem1  35756  dfrdg2  35768  cntotbnd  37775  heiborlem5  37794  heiborlem6  37795  eqvrelsymrel  38575  atl0dm  39280  dalem-ccly  39664  stoweidlem60  46042  fourierdlem40  46129  fourierdlem78  46166  upgrimpthslem1  47892  usgrgrtrirex  47935  ackval40  48679