Theorem simp2bi 1147

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 1144	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 1089

This theorem is referenced by:  0ellim  6389  smodm  8293  erdm  8656  ixpfn  8853  winafp  10620  inar1  10698  inatsk  10701  tskuni  10706  grur1  10743  supmullem1  12124  supmullem2  12125  supmul  12126  eluzelz  12773  elfz3nn0  13549  elfzo0l  13684  ico01fl0  13751  addmodlteq  13881  cshco  14771  swrds2  14875  ef01bndlem  16121  sin01bnd  16122  cos01bnd  16123  sin01gt0  16127  bitsss  16365  smueqlem  16429  gznegcl  16875  gzcjcl  16876  gzaddcl  16877  gzmulcl  16878  gzabssqcl  16881  4sqlem4a  16891  cshwshashlem2  17036  structn0fun  17090  xpsff1o  17500  mre1cl  17525  drsbn0  18239  subgss  19069  symgfixelsi  19376  psgnunilem5  19435  pgpgrp  19535  slwsubg  19551  efgs1b  19677  efgsp1  19678  efgsres  19679  efgredeu  19693  efgred2  19694  efgcpbllemb  19696  omndtos  20068  rngmgp  20103  srgmgp  20138  ringmgp  20186  irrednu  20373  sdrgsubrg  20736  fldsdrgfld  20743  sdrgint  20749  primefld  20750  primefld0cl  20751  primefld1cl  20752  orngogrp  20808  lmodring  20831  lmodprop2d  20887  lssn0  20903  phlsrng  21598  ocvss  21637  obsss  21691  locfinbas  23478  fclsfil  23966  tmdtps  24032  tgptmd  24035  trgring  24127  tdrgdrng  24130  ngpms  24556  icopnfcnv  24908  xrhmeo  24912  oprpiece1res2  24918  phtpcer  24962  pcoval2  24984  pcoass  24992  clmsca  25033  cphsqrtcl  25152  bncms  25312  itg2ge0  25704  uc1pn0  26119  mon1pn0  26120  sinq12ge0  26485  cosq14gt0  26487  cosq14ge0  26488  cos02pilt1  26503  cosq34lt1  26504  sinord  26511  recosf1o  26512  resinf1o  26513  logrnaddcl  26551  logbcl  26745  relogbreexp  26753  atanf  26858  atanneg  26885  atancj  26888  efiatan  26890  atanlogaddlem  26891  atanlogadd  26892  atanlogsub  26894  efiatan2  26895  2efiatan  26896  tanatan  26897  dvatan  26913  areambl  26936  rlimcnp  26943  emgt0  26985  harmoniclbnd  26987  harmonicbnd4  26989  lgamgulmlem2  27008  gausslemma2dlem1a  27344  2sqlem2  27397  2sqlem3  27399  dchrvmasumlem2  27477  dchrvmasumiflem1  27480  logdivbnd  27535  pntpbnd2  27566  pnt  27593  brbtwn2  28990  ax5seglem3  29016  ax5seglem6  29019  axpaschlem  29025  axcontlem2  29050  axcontlem4  29052  crctcshwlkn0lem4  29898  wwlkbp  29926  clwwisshclwwslem  30101  hst1a  32305  stge0  32311  sthil  32321  neldifpr1  32619  f1mptrn  32724  cshwrnid  33053  fsumrp0cl  33113  fzo0pmtrlast  33185  wrdpmtrlast  33186  psgnfzto1stlem  33193  slmdsrg  33300  primefldchr  33394  fldgensdrg  33407  primefldgen1  33414  1arithidomlem1  33627  1arithidomlem2  33628  1arithidom  33629  elunitge0  34076  xrge0iifcnv  34110  xrge0iifcv  34111  xrge0iifiso  34112  rrextnlm  34180  rrextchr  34181  0elros  34347  0elsros  34354  voliune  34406  volfiniune  34407  bnj563  34919  bnj1212  34974  bnj1219  34975  bnj1366  35004  bnj1379  35005  bnj545  35070  bnj594  35087  bnj1118  35159  bnj1177  35181  bnj1190  35183  bnj1398  35209  bnj1417  35216  bnj1450  35225  bnj1312  35233  bnj1523  35246  pthhashvtx  35341  msrval  35751  mclsppslem  35796  dfon2lem1  35994  dfrdg2  36006  cntotbnd  38041  heiborlem5  38060  heiborlem6  38061  eqvrelsymrel  38928  atl0dm  39672  dalem-ccly  40055  stoweidlem60  46412  fourierdlem40  46499  fourierdlem78  46536  upgrimpthslem1  48261  usgrgrtrirex  48304  ackval40  49047