Theorem simp2bi 1164

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 219	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp2d 1161	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  0ellim  6448  smodm  8390  erdm  8759  ixpfn  8962  winafp  10812  inar1  10890  inatsk  10893  tskuni  10898  grur1  10935  supmullem1  12317  supmullem2  12318  supmul  12319  eluzelz  13005  elfz3nn0  13785  elfzo0l  13921  ico01fl0  13989  addmodlteq  14119  cshco  15018  swrds2  15123  ef01bndlem  16384  sin01bnd  16385  cos01bnd  16386  sin01gt0  16390  bitsss  16628  smueqlem  16692  gznegcl  17145  gzcjcl  17146  gzaddcl  17147  gzmulcl  17148  gzabssqcl  17151  4sqlem4a  17161  cshwshashlem2  17306  structn0fun  17361  xpsff1o  17771  mre1cl  17796  drsbn0  18510  subgss  19369  symgfixelsi  19682  psgnunilem5  19741  pgpgrp  19841  slwsubg  19857  efgs1b  19983  efgsp1  19984  efgsres  19985  efgredeu  19999  efgred2  20000  efgcpbllemb  20002  omndtos  20374  rngmgp  20411  srgmgp  20450  ringmgp  20498  irrednu  20688  sdrgsubrg  21081  fldsdrgfld  21088  sdrgint  21094  primefld  21095  primefld0cl  21096  primefld1cl  21097  orngogrp  21153  lmodring  21176  lmodprop2d  21232  lssn0  21248  phlsrng  21970  ocvss  22009  obsss  22063  locfinbas  23874  fclsfil  24362  tmdtps  24428  tgptmd  24431  trgring  24523  tdrgdrng  24526  ngpms  24952  icopnfcnv  25296  xrhmeo  25300  oprpiece1res2  25306  phtpcer  25349  pcoval2  25370  pcoass  25378  clmsca  25419  cphsqrtcl  25538  bncms  25698  itg2ge0  26089  uc1pn0  26497  mon1pn0  26498  sinq12ge0  26870  cosq14gt0  26872  cosq14ge0  26873  cos02pilt1  26887  cosq34lt1  26888  sinord  26895  recosf1o  26896  resinf1o  26897  logrnaddcl  26935  logbcl  27128  relogbreexp  27136  atanf  27241  atanneg  27268  atancj  27271  efiatan  27273  atanlogaddlem  27274  atanlogadd  27275  atanlogsub  27277  efiatan2  27278  2efiatan  27279  tanatan  27280  dvatan  27296  areambl  27319  rlimcnp  27326  emgt0  27367  harmoniclbnd  27369  harmonicbnd4  27371  lgamgulmlem2  27390  gausslemma2dlem1a  27725  2sqlem2  27778  2sqlem3  27780  dchrvmasumlem2  27858  dchrvmasumiflem1  27861  logdivbnd  27916  pntpbnd2  27947  pnt  27974  brbtwn2  29516  ax5seglem3  29542  ax5seglem6  29545  axpaschlem  29551  axcontlem2  29576  axcontlem4  29578  pthhashvtx  30348  crctcshwlkn0lem4  30435  wwlkbp  30463  clwwisshclwwslem  30638  hst1a  32853  stge0  32859  sthil  32869  neldifpr1  33204  f1mptrn  33304  cshwrnid  33595  fsumrp0cl  33658  fzo0pmtrlast  33729  wrdpmtrlast  33730  psgnfzto1stlem  33737  slmdsrg  33844  primefldchr  33947  fldgensdrg  33960  primefldgen1  33967  1arithidomlem1  34151  1arithidomlem2  34152  1arithidom  34153  elunitge0  34614  xrge0iifcnv  34648  xrge0iifcv  34649  xrge0iifiso  34650  rrextnlm  34718  rrextchr  34719  0elros  34886  0elsros  34893  voliune  34945  volfiniune  34946  bnj563  35457  bnj1212  35512  bnj1219  35513  bnj1366  35542  bnj1379  35543  bnj545  35608  bnj594  35625  bnj1118  35697  bnj1177  35719  bnj1190  35721  bnj1398  35747  bnj1417  35754  bnj1450  35763  bnj1312  35771  bnj1523  35784  msrval  36483  mclsppslem  36528  dfrdg2  36748  cntotbnd  38933  heiborlem5  38952  heiborlem6  38953  eqvrelsymrel  39818  atl0dm  40562  dalem-ccly  40945  stoweidlem60  47285  fourierdlem40  47372  fourierdlem78  47409  upgrimpthslem1  49220  usgrgrtrirex  49263  ackval40  50020