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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  0ellim  6381  smodm  8283  erdm  8645  ixpfn  8841  winafp  10608  inar1  10686  inatsk  10689  tskuni  10694  grur1  10731  supmullem1  12112  supmullem2  12113  supmul  12114  eluzelz  12761  elfz3nn0  13537  elfzo0l  13672  ico01fl0  13739  addmodlteq  13869  cshco  14759  swrds2  14863  ef01bndlem  16109  sin01bnd  16110  cos01bnd  16111  sin01gt0  16115  bitsss  16353  smueqlem  16417  gznegcl  16863  gzcjcl  16864  gzaddcl  16865  gzmulcl  16866  gzabssqcl  16869  4sqlem4a  16879  cshwshashlem2  17024  structn0fun  17078  xpsff1o  17488  mre1cl  17513  drsbn0  18227  subgss  19057  symgfixelsi  19364  psgnunilem5  19423  pgpgrp  19523  slwsubg  19539  efgs1b  19665  efgsp1  19666  efgsres  19667  efgredeu  19681  efgred2  19682  efgcpbllemb  19684  omndtos  20056  rngmgp  20091  srgmgp  20126  ringmgp  20174  irrednu  20361  sdrgsubrg  20724  fldsdrgfld  20731  sdrgint  20737  primefld  20738  primefld0cl  20739  primefld1cl  20740  orngogrp  20796  lmodring  20819  lmodprop2d  20875  lssn0  20891  phlsrng  21586  ocvss  21625  obsss  21679  locfinbas  23466  fclsfil  23954  tmdtps  24020  tgptmd  24023  trgring  24115  tdrgdrng  24118  ngpms  24544  icopnfcnv  24896  xrhmeo  24900  oprpiece1res2  24906  phtpcer  24950  pcoval2  24972  pcoass  24980  clmsca  25021  cphsqrtcl  25140  bncms  25300  itg2ge0  25692  uc1pn0  26107  mon1pn0  26108  sinq12ge0  26473  cosq14gt0  26475  cosq14ge0  26476  cos02pilt1  26491  cosq34lt1  26492  sinord  26499  recosf1o  26500  resinf1o  26501  logrnaddcl  26539  logbcl  26733  relogbreexp  26741  atanf  26846  atanneg  26873  atancj  26876  efiatan  26878  atanlogaddlem  26879  atanlogadd  26880  atanlogsub  26882  efiatan2  26883  2efiatan  26884  tanatan  26885  dvatan  26901  areambl  26924  rlimcnp  26931  emgt0  26973  harmoniclbnd  26975  harmonicbnd4  26977  lgamgulmlem2  26996  gausslemma2dlem1a  27332  2sqlem2  27385  2sqlem3  27387  dchrvmasumlem2  27465  dchrvmasumiflem1  27468  logdivbnd  27523  pntpbnd2  27554  pnt  27581  brbtwn2  28978  ax5seglem3  29004  ax5seglem6  29007  axpaschlem  29013  axcontlem2  29038  axcontlem4  29040  crctcshwlkn0lem4  29886  wwlkbp  29914  clwwisshclwwslem  30089  hst1a  32293  stge0  32299  sthil  32309  neldifpr1  32608  f1mptrn  32713  cshwrnid  33043  fsumrp0cl  33103  fzo0pmtrlast  33174  wrdpmtrlast  33175  psgnfzto1stlem  33182  slmdsrg  33289  primefldchr  33383  fldgensdrg  33396  primefldgen1  33403  1arithidomlem1  33616  1arithidomlem2  33617  1arithidom  33618  elunitge0  34056  xrge0iifcnv  34090  xrge0iifcv  34091  xrge0iifiso  34092  rrextnlm  34160  rrextchr  34161  0elros  34327  0elsros  34334  voliune  34386  volfiniune  34387  bnj563  34899  bnj1212  34955  bnj1219  34956  bnj1366  34985  bnj1379  34986  bnj545  35051  bnj594  35068  bnj1118  35140  bnj1177  35162  bnj1190  35164  bnj1398  35190  bnj1417  35197  bnj1450  35206  bnj1312  35214  bnj1523  35227  pthhashvtx  35322  msrval  35732  mclsppslem  35777  dfon2lem1  35975  dfrdg2  35987  cntotbnd  37993  heiborlem5  38012  heiborlem6  38013  eqvrelsymrel  38852  atl0dm  39558  dalem-ccly  39941  stoweidlem60  46300  fourierdlem40  46387  fourierdlem78  46424  upgrimpthslem1  48149  usgrgrtrirex  48192  ackval40  48935