Theorem simp2bi 1147

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  smodm  8351  erdm  8713  ixpfn  8897  winafp  10692  inar1  10770  inatsk  10773  tskuni  10778  grur1  10815  supmullem1  12184  supmullem2  12185  supmul  12186  eluzelz  12832  elfz3nn0  13595  elfzo0l  13722  ico01fl0  13784  addmodlteq  13911  cshco  14787  swrds2  14891  ef01bndlem  16127  sin01bnd  16128  cos01bnd  16129  sin01gt0  16133  bitsss  16367  smueqlem  16431  gznegcl  16868  gzcjcl  16869  gzaddcl  16870  gzmulcl  16871  gzabssqcl  16874  4sqlem4a  16884  cshwshashlem2  17030  structn0fun  17084  xpsff1o  17513  mre1cl  17538  drsbn0  18257  subgss  19007  symgfixelsi  19303  psgnunilem5  19362  pgpgrp  19462  slwsubg  19478  efgs1b  19604  efgsp1  19605  efgsres  19606  efgredeu  19620  efgred2  19621  efgcpbllemb  19623  srgmgp  20014  ringmgp  20062  irrednu  20239  sdrgsubrg  20407  fldsdrgfld  20414  sdrgint  20420  primefld  20421  primefld0cl  20422  primefld1cl  20423  lmodring  20479  lmodprop2d  20534  lssn0  20551  phlsrng  21184  ocvss  21223  obsss  21279  locfinbas  23026  fclsfil  23514  tmdtps  23580  tgptmd  23583  trgring  23675  tdrgdrng  23678  ngpms  24109  icopnfcnv  24458  xrhmeo  24462  oprpiece1res2  24468  phtpcer  24511  pcoval2  24532  pcoass  24540  clmsca  24581  cphsqrtcl  24701  bncms  24861  itg2ge0  25253  uc1pn0  25663  mon1pn0  25664  sinq12ge0  26018  cosq14gt0  26020  cosq14ge0  26021  cos02pilt1  26035  cosq34lt1  26036  sinord  26043  recosf1o  26044  resinf1o  26045  logrnaddcl  26083  logbcl  26272  relogbreexp  26280  atanf  26385  atanneg  26412  atancj  26415  efiatan  26417  atanlogaddlem  26418  atanlogadd  26419  atanlogsub  26421  efiatan2  26422  2efiatan  26423  tanatan  26424  dvatan  26440  areambl  26463  rlimcnp  26470  emgt0  26511  harmoniclbnd  26513  harmonicbnd4  26515  lgamgulmlem2  26534  gausslemma2dlem1a  26868  2sqlem2  26921  2sqlem3  26923  dchrvmasumlem2  27001  dchrvmasumiflem1  27004  logdivbnd  27059  pntpbnd2  27090  pnt  27117  brbtwn2  28163  ax5seglem3  28189  ax5seglem6  28192  axpaschlem  28198  axcontlem2  28223  axcontlem4  28225  crctcshwlkn0lem4  29067  wwlkbp  29095  clwwisshclwwslem  29267  hst1a  31471  stge0  31477  sthil  31487  neldifpr1  31770  f1mptrn  31859  cshwrnid  32125  fsumrp0cl  32196  omndtos  32223  psgnfzto1stlem  32259  slmdsrg  32352  primefldchr  32399  fldgensdrg  32404  primefldgen1  32411  orngogrp  32419  elunitge0  32879  xrge0iifcnv  32913  xrge0iifcv  32914  xrge0iifiso  32915  rrextnlm  32983  rrextchr  32984  0elros  33168  0elsros  33175  voliune  33227  volfiniune  33228  bnj563  33754  bnj1212  33810  bnj1219  33811  bnj1366  33840  bnj1379  33841  bnj545  33906  bnj594  33923  bnj1118  33995  bnj1177  34017  bnj1190  34019  bnj1398  34045  bnj1417  34052  bnj1450  34061  bnj1312  34069  bnj1523  34082  pthhashvtx  34118  msrval  34529  mclsppslem  34574  dfon2lem1  34755  dfrdg2  34767  cntotbnd  36664  heiborlem5  36683  heiborlem6  36684  eqvrelsymrel  37469  atl0dm  38172  dalem-ccly  38556  stoweidlem60  44776  fourierdlem40  44863  fourierdlem78  44900  rngmgp  46652  ackval40  47379