Theorem simp2bi 1162

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

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

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 1103

This theorem is referenced by:  0ellim  6414  smodm  8326  erdm  8693  ixpfn  8889  winafp  10670  inar1  10748  inatsk  10751  tskuni  10756  grur1  10793  supmullem1  12176  supmullem2  12177  supmul  12178  eluzelz  12863  elfz3nn0  13640  elfzo0l  13776  ico01fl0  13843  addmodlteq  13973  cshco  14863  swrds2  14967  ef01bndlem  16230  sin01bnd  16231  cos01bnd  16232  sin01gt0  16236  bitsss  16474  smueqlem  16538  gznegcl  16985  gzcjcl  16986  gzaddcl  16987  gzmulcl  16988  gzabssqcl  16991  4sqlem4a  17001  cshwshashlem2  17146  structn0fun  17201  xpsff1o  17611  mre1cl  17636  drsbn0  18350  subgss  19184  symgfixelsi  19496  psgnunilem5  19555  pgpgrp  19655  slwsubg  19671  efgs1b  19797  efgsp1  19798  efgsres  19799  efgredeu  19813  efgred2  19814  efgcpbllemb  19816  omndtos  20188  rngmgp  20225  srgmgp  20264  ringmgp  20312  irrednu  20498  sdrgsubrg  20863  fldsdrgfld  20870  sdrgint  20876  primefld  20877  primefld0cl  20878  primefld1cl  20879  orngogrp  20935  lmodring  20958  lmodprop2d  21014  lssn0  21030  phlsrng  21741  ocvss  21780  obsss  21834  locfinbas  23640  fclsfil  24128  tmdtps  24194  tgptmd  24197  trgring  24289  tdrgdrng  24292  ngpms  24718  icopnfcnv  25062  xrhmeo  25066  oprpiece1res2  25072  phtpcer  25115  pcoval2  25136  pcoass  25144  clmsca  25185  cphsqrtcl  25304  bncms  25464  itg2ge0  25855  uc1pn0  26264  mon1pn0  26265  sinq12ge0  26631  cosq14gt0  26633  cosq14ge0  26634  cos02pilt1  26649  cosq34lt1  26650  sinord  26657  recosf1o  26658  resinf1o  26659  logrnaddcl  26697  logbcl  26890  relogbreexp  26898  atanf  27003  atanneg  27030  atancj  27033  efiatan  27035  atanlogaddlem  27036  atanlogadd  27037  atanlogsub  27039  efiatan2  27040  2efiatan  27041  tanatan  27042  dvatan  27058  areambl  27081  rlimcnp  27088  emgt0  27129  harmoniclbnd  27131  harmonicbnd4  27133  lgamgulmlem2  27152  gausslemma2dlem1a  27487  2sqlem2  27540  2sqlem3  27542  dchrvmasumlem2  27620  dchrvmasumiflem1  27623  logdivbnd  27678  pntpbnd2  27709  pnt  27736  brbtwn2  29164  ax5seglem3  29190  ax5seglem6  29193  axpaschlem  29199  axcontlem2  29224  axcontlem4  29226  crctcshwlkn0lem4  30071  wwlkbp  30099  clwwisshclwwslem  30274  hst1a  32479  stge0  32485  sthil  32495  neldifpr1  32789  f1mptrn  32892  cshwrnid  33194  fsumrp0cl  33254  fzo0pmtrlast  33325  wrdpmtrlast  33326  psgnfzto1stlem  33333  slmdsrg  33440  primefldchr  33537  fldgensdrg  33550  primefldgen1  33557  1arithidomlem1  33742  1arithidomlem2  33743  1arithidom  33744  elunitge0  34206  xrge0iifcnv  34240  xrge0iifcv  34241  xrge0iifiso  34242  rrextnlm  34310  rrextchr  34311  0elros  34477  0elsros  34484  voliune  34536  volfiniune  34537  bnj563  35049  bnj1212  35104  bnj1219  35105  bnj1366  35134  bnj1379  35135  bnj545  35200  bnj594  35217  bnj1118  35289  bnj1177  35311  bnj1190  35313  bnj1398  35339  bnj1417  35346  bnj1450  35355  bnj1312  35363  bnj1523  35376  pthhashvtx  35491  msrval  35901  mclsppslem  35946  dfon2lem1  36144  dfrdg2  36156  cntotbnd  38307  heiborlem5  38326  heiborlem6  38327  eqvrelsymrel  39194  atl0dm  39938  dalem-ccly  40321  stoweidlem60  46632  fourierdlem40  46719  fourierdlem78  46756  upgrimpthslem1  48527  usgrgrtrirex  48570  ackval40  49324