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

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

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 1105

This theorem is referenced by:  0ellim  6427  smodm  8339  erdm  8706  ixpfn  8902  winafp  10683  inar1  10761  inatsk  10764  tskuni  10769  grur1  10806  supmullem1  12186  supmullem2  12187  supmul  12188  eluzelz  12873  elfz3nn0  13651  elfzo0l  13787  ico01fl0  13854  addmodlteq  13984  cshco  14875  swrds2  14979  ef01bndlem  16241  sin01bnd  16242  cos01bnd  16243  sin01gt0  16247  bitsss  16485  smueqlem  16549  gznegcl  16996  gzcjcl  16997  gzaddcl  16998  gzmulcl  16999  gzabssqcl  17002  4sqlem4a  17012  cshwshashlem2  17157  structn0fun  17212  xpsff1o  17622  mre1cl  17647  drsbn0  18361  subgss  19194  symgfixelsi  19506  psgnunilem5  19565  pgpgrp  19665  slwsubg  19681  efgs1b  19807  efgsp1  19808  efgsres  19809  efgredeu  19823  efgred2  19824  efgcpbllemb  19826  omndtos  20198  rngmgp  20235  srgmgp  20274  ringmgp  20322  irrednu  20508  sdrgsubrg  20875  fldsdrgfld  20882  sdrgint  20888  primefld  20889  primefld0cl  20890  primefld1cl  20891  orngogrp  20947  lmodring  20970  lmodprop2d  21026  lssn0  21042  phlsrng  21762  ocvss  21801  obsss  21855  locfinbas  23660  fclsfil  24148  tmdtps  24214  tgptmd  24217  trgring  24309  tdrgdrng  24312  ngpms  24738  icopnfcnv  25082  xrhmeo  25086  oprpiece1res2  25092  phtpcer  25135  pcoval2  25156  pcoass  25164  clmsca  25205  cphsqrtcl  25324  bncms  25484  itg2ge0  25875  uc1pn0  26284  mon1pn0  26285  sinq12ge0  26654  cosq14gt0  26656  cosq14ge0  26657  cos02pilt1  26672  cosq34lt1  26673  sinord  26680  recosf1o  26681  resinf1o  26682  logrnaddcl  26720  logbcl  26913  relogbreexp  26921  atanf  27026  atanneg  27053  atancj  27056  efiatan  27058  atanlogaddlem  27059  atanlogadd  27060  atanlogsub  27062  efiatan2  27063  2efiatan  27064  tanatan  27065  dvatan  27081  areambl  27104  rlimcnp  27111  emgt0  27152  harmoniclbnd  27154  harmonicbnd4  27156  lgamgulmlem2  27175  gausslemma2dlem1a  27510  2sqlem2  27563  2sqlem3  27565  dchrvmasumlem2  27643  dchrvmasumiflem1  27646  logdivbnd  27701  pntpbnd2  27732  pnt  27759  brbtwn2  29236  ax5seglem3  29262  ax5seglem6  29265  axpaschlem  29271  axcontlem2  29296  axcontlem4  29298  crctcshwlkn0lem4  30143  wwlkbp  30171  clwwisshclwwslem  30346  hst1a  32551  stge0  32557  sthil  32567  neldifpr1  32860  f1mptrn  32961  cshwrnid  33262  fsumrp0cl  33322  fzo0pmtrlast  33393  wrdpmtrlast  33394  psgnfzto1stlem  33401  slmdsrg  33508  primefldchr  33603  fldgensdrg  33616  primefldgen1  33623  1arithidomlem1  33806  1arithidomlem2  33807  1arithidom  33808  elunitge0  34270  xrge0iifcnv  34304  xrge0iifcv  34305  xrge0iifiso  34306  rrextnlm  34374  rrextchr  34375  0elros  34541  0elsros  34548  voliune  34600  volfiniune  34601  bnj563  35113  bnj1212  35168  bnj1219  35169  bnj1366  35198  bnj1379  35199  bnj545  35264  bnj594  35281  bnj1118  35353  bnj1177  35375  bnj1190  35377  bnj1398  35403  bnj1417  35410  bnj1450  35419  bnj1312  35427  bnj1523  35440  pthhashvtx  35601  msrval  36011  mclsppslem  36056  dfon2lem1  36254  dfrdg2  36266  cntotbnd  38428  heiborlem5  38447  heiborlem6  38448  eqvrelsymrel  39313  atl0dm  40057  dalem-ccly  40440  stoweidlem60  46757  fourierdlem40  46844  fourierdlem78  46881  upgrimpthslem1  48655  usgrgrtrirex  48698  ackval40  49456