Theorem simp2bi 1162

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  0ellim  6414  smodm  8326  erdm  8693  ixpfn  8889  winafp  10670  inar1  10748  inatsk  10751  tskuni  10756  grur1  10793  supmullem1  12173  supmullem2  12174  supmul  12175  eluzelz  12860  elfz3nn0  13637  elfzo0l  13773  ico01fl0  13840  addmodlteq  13970  cshco  14861  swrds2  14965  ef01bndlem  16228  sin01bnd  16229  cos01bnd  16230  sin01gt0  16234  bitsss  16472  smueqlem  16536  gznegcl  16983  gzcjcl  16984  gzaddcl  16985  gzmulcl  16986  gzabssqcl  16989  4sqlem4a  16999  cshwshashlem2  17144  structn0fun  17199  xpsff1o  17609  mre1cl  17634  drsbn0  18348  subgss  19181  symgfixelsi  19493  psgnunilem5  19552  pgpgrp  19652  slwsubg  19668  efgs1b  19794  efgsp1  19795  efgsres  19796  efgredeu  19810  efgred2  19811  efgcpbllemb  19813  omndtos  20185  rngmgp  20222  srgmgp  20261  ringmgp  20309  irrednu  20495  sdrgsubrg  20860  fldsdrgfld  20867  sdrgint  20873  primefld  20874  primefld0cl  20875  primefld1cl  20876  orngogrp  20932  lmodring  20955  lmodprop2d  21011  lssn0  21027  phlsrng  21738  ocvss  21777  obsss  21831  locfinbas  23636  fclsfil  24124  tmdtps  24190  tgptmd  24193  trgring  24285  tdrgdrng  24288  ngpms  24714  icopnfcnv  25058  xrhmeo  25062  oprpiece1res2  25068  phtpcer  25111  pcoval2  25132  pcoass  25140  clmsca  25181  cphsqrtcl  25300  bncms  25460  itg2ge0  25851  uc1pn0  26260  mon1pn0  26261  sinq12ge0  26627  cosq14gt0  26629  cosq14ge0  26630  cos02pilt1  26645  cosq34lt1  26646  sinord  26653  recosf1o  26654  resinf1o  26655  logrnaddcl  26693  logbcl  26886  relogbreexp  26894  atanf  26999  atanneg  27026  atancj  27029  efiatan  27031  atanlogaddlem  27032  atanlogadd  27033  atanlogsub  27035  efiatan2  27036  2efiatan  27037  tanatan  27038  dvatan  27054  areambl  27077  rlimcnp  27084  emgt0  27125  harmoniclbnd  27127  harmonicbnd4  27129  lgamgulmlem2  27148  gausslemma2dlem1a  27483  2sqlem2  27536  2sqlem3  27538  dchrvmasumlem2  27616  dchrvmasumiflem1  27619  logdivbnd  27674  pntpbnd2  27705  pnt  27732  brbtwn2  29160  ax5seglem3  29186  ax5seglem6  29189  axpaschlem  29195  axcontlem2  29220  axcontlem4  29222  crctcshwlkn0lem4  30067  wwlkbp  30095  clwwisshclwwslem  30270  hst1a  32475  stge0  32481  sthil  32491  neldifpr1  32785  f1mptrn  32888  cshwrnid  33189  fsumrp0cl  33249  fzo0pmtrlast  33320  wrdpmtrlast  33321  psgnfzto1stlem  33328  slmdsrg  33435  primefldchr  33532  fldgensdrg  33545  primefldgen1  33552  1arithidomlem1  33737  1arithidomlem2  33738  1arithidom  33739  elunitge0  34201  xrge0iifcnv  34235  xrge0iifcv  34236  xrge0iifiso  34237  rrextnlm  34305  rrextchr  34306  0elros  34472  0elsros  34479  voliune  34531  volfiniune  34532  bnj563  35044  bnj1212  35099  bnj1219  35100  bnj1366  35129  bnj1379  35130  bnj545  35195  bnj594  35212  bnj1118  35284  bnj1177  35306  bnj1190  35308  bnj1398  35334  bnj1417  35341  bnj1450  35350  bnj1312  35358  bnj1523  35371  pthhashvtx  35486  msrval  35896  mclsppslem  35941  dfon2lem1  36139  dfrdg2  36151  cntotbnd  38302  heiborlem5  38321  heiborlem6  38322  eqvrelsymrel  39189  atl0dm  39933  dalem-ccly  40316  stoweidlem60  46633  fourierdlem40  46720  fourierdlem78  46757  upgrimpthslem1  48528  usgrgrtrirex  48571  ackval40  49325