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  6381  smodm  8284  erdm  8647  ixpfn  8844  winafp  10611  inar1  10689  inatsk  10692  tskuni  10697  grur1  10734  supmullem1  12117  supmullem2  12118  supmul  12119  eluzelz  12789  elfz3nn0  13566  elfzo0l  13702  ico01fl0  13769  addmodlteq  13899  cshco  14789  swrds2  14893  ef01bndlem  16142  sin01bnd  16143  cos01bnd  16144  sin01gt0  16148  bitsss  16386  smueqlem  16450  gznegcl  16897  gzcjcl  16898  gzaddcl  16899  gzmulcl  16900  gzabssqcl  16903  4sqlem4a  16913  cshwshashlem2  17058  structn0fun  17112  xpsff1o  17522  mre1cl  17547  drsbn0  18261  subgss  19094  symgfixelsi  19401  psgnunilem5  19460  pgpgrp  19560  slwsubg  19576  efgs1b  19702  efgsp1  19703  efgsres  19704  efgredeu  19718  efgred2  19719  efgcpbllemb  19721  omndtos  20093  rngmgp  20128  srgmgp  20163  ringmgp  20211  irrednu  20396  sdrgsubrg  20759  fldsdrgfld  20766  sdrgint  20772  primefld  20773  primefld0cl  20774  primefld1cl  20775  orngogrp  20831  lmodring  20854  lmodprop2d  20910  lssn0  20926  phlsrng  21621  ocvss  21660  obsss  21714  locfinbas  23497  fclsfil  23985  tmdtps  24051  tgptmd  24054  trgring  24146  tdrgdrng  24149  ngpms  24575  icopnfcnv  24919  xrhmeo  24923  oprpiece1res2  24929  phtpcer  24972  pcoval2  24993  pcoass  25001  clmsca  25042  cphsqrtcl  25161  bncms  25321  itg2ge0  25712  uc1pn0  26121  mon1pn0  26122  sinq12ge0  26485  cosq14gt0  26487  cosq14ge0  26488  cos02pilt1  26503  cosq34lt1  26504  sinord  26511  recosf1o  26512  resinf1o  26513  logrnaddcl  26551  logbcl  26744  relogbreexp  26752  atanf  26857  atanneg  26884  atancj  26887  efiatan  26889  atanlogaddlem  26890  atanlogadd  26891  atanlogsub  26893  efiatan2  26894  2efiatan  26895  tanatan  26896  dvatan  26912  areambl  26935  rlimcnp  26942  emgt0  26984  harmoniclbnd  26986  harmonicbnd4  26988  lgamgulmlem2  27007  gausslemma2dlem1a  27342  2sqlem2  27395  2sqlem3  27397  dchrvmasumlem2  27475  dchrvmasumiflem1  27478  logdivbnd  27533  pntpbnd2  27564  pnt  27591  brbtwn2  28988  ax5seglem3  29014  ax5seglem6  29017  axpaschlem  29023  axcontlem2  29048  axcontlem4  29050  crctcshwlkn0lem4  29896  wwlkbp  29924  clwwisshclwwslem  30099  hst1a  32304  stge0  32310  sthil  32320  neldifpr1  32618  f1mptrn  32723  cshwrnid  33036  fsumrp0cl  33096  fzo0pmtrlast  33168  wrdpmtrlast  33169  psgnfzto1stlem  33176  slmdsrg  33283  primefldchr  33377  fldgensdrg  33390  primefldgen1  33397  1arithidomlem1  33610  1arithidomlem2  33611  1arithidom  33612  elunitge0  34059  xrge0iifcnv  34093  xrge0iifcv  34094  xrge0iifiso  34095  rrextnlm  34163  rrextchr  34164  0elros  34330  0elsros  34337  voliune  34389  volfiniune  34390  bnj563  34902  bnj1212  34957  bnj1219  34958  bnj1366  34987  bnj1379  34988  bnj545  35053  bnj594  35070  bnj1118  35142  bnj1177  35164  bnj1190  35166  bnj1398  35192  bnj1417  35199  bnj1450  35208  bnj1312  35216  bnj1523  35229  pthhashvtx  35326  msrval  35736  mclsppslem  35781  dfon2lem1  35979  dfrdg2  35991  cntotbnd  38131  heiborlem5  38150  heiborlem6  38151  eqvrelsymrel  39018  atl0dm  39762  dalem-ccly  40145  stoweidlem60  46506  fourierdlem40  46593  fourierdlem78  46630  upgrimpthslem1  48395  usgrgrtrirex  48438  ackval40  49181