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  6370  smodm  8271  erdm  8632  ixpfn  8827  winafp  10585  inar1  10663  inatsk  10666  tskuni  10671  grur1  10708  supmullem1  12089  supmullem2  12090  supmul  12091  eluzelz  12739  elfz3nn0  13518  elfzo0l  13653  ico01fl0  13720  addmodlteq  13850  cshco  14740  swrds2  14844  ef01bndlem  16090  sin01bnd  16091  cos01bnd  16092  sin01gt0  16096  bitsss  16334  smueqlem  16398  gznegcl  16844  gzcjcl  16845  gzaddcl  16846  gzmulcl  16847  gzabssqcl  16850  4sqlem4a  16860  cshwshashlem2  17005  structn0fun  17059  xpsff1o  17468  mre1cl  17493  drsbn0  18207  subgss  19037  symgfixelsi  19345  psgnunilem5  19404  pgpgrp  19504  slwsubg  19520  efgs1b  19646  efgsp1  19647  efgsres  19648  efgredeu  19662  efgred2  19663  efgcpbllemb  19665  omndtos  20037  rngmgp  20072  srgmgp  20107  ringmgp  20155  irrednu  20341  sdrgsubrg  20704  fldsdrgfld  20711  sdrgint  20717  primefld  20718  primefld0cl  20719  primefld1cl  20720  orngogrp  20776  lmodring  20799  lmodprop2d  20855  lssn0  20871  phlsrng  21566  ocvss  21605  obsss  21659  locfinbas  23435  fclsfil  23923  tmdtps  23989  tgptmd  23992  trgring  24084  tdrgdrng  24087  ngpms  24513  icopnfcnv  24865  xrhmeo  24869  oprpiece1res2  24875  phtpcer  24919  pcoval2  24941  pcoass  24949  clmsca  24990  cphsqrtcl  25109  bncms  25269  itg2ge0  25661  uc1pn0  26076  mon1pn0  26077  sinq12ge0  26442  cosq14gt0  26444  cosq14ge0  26445  cos02pilt1  26460  cosq34lt1  26461  sinord  26468  recosf1o  26469  resinf1o  26470  logrnaddcl  26508  logbcl  26702  relogbreexp  26710  atanf  26815  atanneg  26842  atancj  26845  efiatan  26847  atanlogaddlem  26848  atanlogadd  26849  atanlogsub  26851  efiatan2  26852  2efiatan  26853  tanatan  26854  dvatan  26870  areambl  26893  rlimcnp  26900  emgt0  26942  harmoniclbnd  26944  harmonicbnd4  26946  lgamgulmlem2  26965  gausslemma2dlem1a  27301  2sqlem2  27354  2sqlem3  27356  dchrvmasumlem2  27434  dchrvmasumiflem1  27437  logdivbnd  27492  pntpbnd2  27523  pnt  27550  brbtwn2  28881  ax5seglem3  28907  ax5seglem6  28910  axpaschlem  28916  axcontlem2  28941  axcontlem4  28943  crctcshwlkn0lem4  29789  wwlkbp  29817  clwwisshclwwslem  29989  hst1a  32193  stge0  32199  sthil  32209  neldifpr1  32508  f1mptrn  32612  cshwrnid  32937  fsumrp0cl  32997  fzo0pmtrlast  33056  wrdpmtrlast  33057  psgnfzto1stlem  33064  slmdsrg  33171  primefldchr  33262  fldgensdrg  33275  primefldgen1  33282  1arithidomlem1  33495  1arithidomlem2  33496  1arithidom  33497  elunitge0  33907  xrge0iifcnv  33941  xrge0iifcv  33942  xrge0iifiso  33943  rrextnlm  34011  rrextchr  34012  0elros  34178  0elsros  34185  voliune  34237  volfiniune  34238  bnj563  34750  bnj1212  34806  bnj1219  34807  bnj1366  34836  bnj1379  34837  bnj545  34902  bnj594  34919  bnj1118  34991  bnj1177  35013  bnj1190  35015  bnj1398  35041  bnj1417  35048  bnj1450  35057  bnj1312  35065  bnj1523  35078  pthhashvtx  35160  msrval  35570  mclsppslem  35615  dfon2lem1  35816  dfrdg2  35828  cntotbnd  37835  heiborlem5  37854  heiborlem6  37855  eqvrelsymrel  38635  atl0dm  39340  dalem-ccly  39723  stoweidlem60  46097  fourierdlem40  46184  fourierdlem78  46221  upgrimpthslem1  47937  usgrgrtrirex  47980  ackval40  48724