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  6432  smodm  8347  erdm  8714  ixpfn  8910  winafp  10700  inar1  10778  inatsk  10781  tskuni  10786  grur1  10823  supmullem1  12203  supmullem2  12204  supmul  12205  eluzelz  12890  elfz3nn0  13668  elfzo0l  13804  ico01fl0  13872  addmodlteq  14002  cshco  14899  swrds2  15003  ef01bndlem  16265  sin01bnd  16266  cos01bnd  16267  sin01gt0  16271  bitsss  16509  smueqlem  16573  gznegcl  17020  gzcjcl  17021  gzaddcl  17022  gzmulcl  17023  gzabssqcl  17026  4sqlem4a  17036  cshwshashlem2  17181  structn0fun  17236  xpsff1o  17646  mre1cl  17671  drsbn0  18385  subgss  19224  symgfixelsi  19536  psgnunilem5  19595  pgpgrp  19695  slwsubg  19711  efgs1b  19837  efgsp1  19838  efgsres  19839  efgredeu  19853  efgred2  19854  efgcpbllemb  19856  omndtos  20228  rngmgp  20265  srgmgp  20304  ringmgp  20352  irrednu  20540  sdrgsubrg  20931  fldsdrgfld  20938  sdrgint  20944  primefld  20945  primefld0cl  20946  primefld1cl  20947  orngogrp  21003  lmodring  21026  lmodprop2d  21082  lssn0  21098  phlsrng  21818  ocvss  21857  obsss  21911  locfinbas  23716  fclsfil  24204  tmdtps  24270  tgptmd  24273  trgring  24365  tdrgdrng  24368  ngpms  24794  icopnfcnv  25138  xrhmeo  25142  oprpiece1res2  25148  phtpcer  25191  pcoval2  25212  pcoass  25220  clmsca  25261  cphsqrtcl  25380  bncms  25540  itg2ge0  25931  uc1pn0  26340  mon1pn0  26341  sinq12ge0  26710  cosq14gt0  26712  cosq14ge0  26713  cos02pilt1  26728  cosq34lt1  26729  sinord  26736  recosf1o  26737  resinf1o  26738  logrnaddcl  26776  logbcl  26969  relogbreexp  26977  atanf  27082  atanneg  27109  atancj  27112  efiatan  27114  atanlogaddlem  27115  atanlogadd  27116  atanlogsub  27118  efiatan2  27119  2efiatan  27120  tanatan  27121  dvatan  27137  areambl  27160  rlimcnp  27167  emgt0  27208  harmoniclbnd  27210  harmonicbnd4  27212  lgamgulmlem2  27231  gausslemma2dlem1a  27566  2sqlem2  27619  2sqlem3  27621  dchrvmasumlem2  27699  dchrvmasumiflem1  27702  logdivbnd  27757  pntpbnd2  27788  pnt  27815  brbtwn2  29292  ax5seglem3  29318  ax5seglem6  29321  axpaschlem  29327  axcontlem2  29352  axcontlem4  29354  crctcshwlkn0lem4  30199  wwlkbp  30227  clwwisshclwwslem  30402  hst1a  32607  stge0  32613  sthil  32623  neldifpr1  32916  f1mptrn  33017  cshwrnid  33312  fsumrp0cl  33372  fzo0pmtrlast  33443  wrdpmtrlast  33444  psgnfzto1stlem  33451  slmdsrg  33558  primefldchr  33653  fldgensdrg  33666  primefldgen1  33673  1arithidomlem1  33856  1arithidomlem2  33857  1arithidom  33858  elunitge0  34320  xrge0iifcnv  34354  xrge0iifcv  34355  xrge0iifiso  34356  rrextnlm  34424  rrextchr  34425  0elros  34592  0elsros  34599  voliune  34651  volfiniune  34652  bnj563  35164  bnj1212  35219  bnj1219  35220  bnj1366  35249  bnj1379  35250  bnj545  35315  bnj594  35332  bnj1118  35404  bnj1177  35426  bnj1190  35428  bnj1398  35454  bnj1417  35461  bnj1450  35470  bnj1312  35478  bnj1523  35491  pthhashvtx  35641  msrval  36051  mclsppslem  36096  dfon2lem1  36294  dfrdg2  36306  cntotbnd  38488  heiborlem5  38507  heiborlem6  38508  eqvrelsymrel  39373  atl0dm  40117  dalem-ccly  40500  stoweidlem60  46815  fourierdlem40  46902  fourierdlem78  46939  upgrimpthslem1  48713  usgrgrtrirex  48756  ackval40  49514