Theorem simp2bi 1146

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  smodm  8302  erdm  8665  ixpfn  8848  winafp  10642  inar1  10720  inatsk  10723  tskuni  10728  grur1  10765  supmullem1  12134  supmullem2  12135  supmul  12136  eluzelz  12782  elfz3nn0  13545  elfzo0l  13672  ico01fl0  13734  addmodlteq  13861  cshco  14737  swrds2  14841  ef01bndlem  16077  sin01bnd  16078  cos01bnd  16079  sin01gt0  16083  bitsss  16317  smueqlem  16381  gznegcl  16818  gzcjcl  16819  gzaddcl  16820  gzmulcl  16821  gzabssqcl  16824  4sqlem4a  16834  cshwshashlem2  16980  structn0fun  17034  xpsff1o  17463  mre1cl  17488  drsbn0  18207  subgss  18943  symgfixelsi  19231  psgnunilem5  19290  pgpgrp  19390  slwsubg  19406  efgs1b  19532  efgsp1  19533  efgsres  19534  efgredeu  19548  efgred2  19549  efgcpbllemb  19551  srgmgp  19936  ringmgp  19984  irrednu  20150  sdrgsubrg  20314  fldsdrgfld  20321  sdrgint  20327  primefld  20328  primefld0cl  20329  primefld1cl  20330  lmodring  20386  lmodprop2d  20441  lssn0  20458  phlsrng  21072  ocvss  21111  obsss  21167  locfinbas  22910  fclsfil  23398  tmdtps  23464  tgptmd  23467  trgring  23559  tdrgdrng  23562  ngpms  23993  icopnfcnv  24342  xrhmeo  24346  oprpiece1res2  24352  phtpcer  24395  pcoval2  24416  pcoass  24424  clmsca  24465  cphsqrtcl  24585  bncms  24745  itg2ge0  25137  uc1pn0  25547  mon1pn0  25548  sinq12ge0  25902  cosq14gt0  25904  cosq14ge0  25905  cos02pilt1  25919  cosq34lt1  25920  sinord  25927  recosf1o  25928  resinf1o  25929  logrnaddcl  25967  logbcl  26154  relogbreexp  26162  atanf  26267  atanneg  26294  atancj  26297  efiatan  26299  atanlogaddlem  26300  atanlogadd  26301  atanlogsub  26303  efiatan2  26304  2efiatan  26305  tanatan  26306  dvatan  26322  areambl  26345  rlimcnp  26352  emgt0  26393  harmoniclbnd  26395  harmonicbnd4  26397  lgamgulmlem2  26416  gausslemma2dlem1a  26750  2sqlem2  26803  2sqlem3  26805  dchrvmasumlem2  26883  dchrvmasumiflem1  26886  logdivbnd  26941  pntpbnd2  26972  pnt  26999  brbtwn2  27917  ax5seglem3  27943  ax5seglem6  27946  axpaschlem  27952  axcontlem2  27977  axcontlem4  27979  crctcshwlkn0lem4  28821  wwlkbp  28849  clwwisshclwwslem  29021  hst1a  31223  stge0  31229  sthil  31239  neldifpr1  31524  f1mptrn  31616  cshwrnid  31885  fsumrp0cl  31956  omndtos  31983  psgnfzto1stlem  32019  slmdsrg  32112  primefldchr  32147  fldgensdrg  32152  primefldgen1  32159  orngogrp  32167  elunitge0  32569  xrge0iifcnv  32603  xrge0iifcv  32604  xrge0iifiso  32605  rrextnlm  32673  rrextchr  32674  0elros  32858  0elsros  32865  voliune  32917  volfiniune  32918  bnj563  33444  bnj1212  33500  bnj1219  33501  bnj1366  33530  bnj1379  33531  bnj545  33596  bnj594  33613  bnj1118  33685  bnj1177  33707  bnj1190  33709  bnj1398  33735  bnj1417  33742  bnj1450  33751  bnj1312  33759  bnj1523  33772  pthhashvtx  33808  msrval  34219  mclsppslem  34264  dfon2lem1  34444  dfrdg2  34456  cntotbnd  36328  heiborlem5  36347  heiborlem6  36348  eqvrelsymrel  37134  atl0dm  37837  dalem-ccly  38221  stoweidlem60  44421  fourierdlem40  44508  fourierdlem78  44545  rngmgp  46296  ackval40  46899