Theorem simp2bi 1070

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  smodm  7335  erdm  7639  ixpfn  7800  winafp  9398  inar1  9476  inatsk  9479  tskuni  9484  grur1  9521  supmullem1  10870  supmullem2  10871  supmul  10872  eluzelz  11573  elfz3nn0  12303  ico01fl0  12482  addmodlteq  12607  cshco  13433  swrds2  13533  ef01bndlem  14753  sin01bnd  14754  cos01bnd  14755  sin01gt0  14759  bitsss  14986  smueqlem  15050  gznegcl  15477  gzcjcl  15478  gzaddcl  15479  gzmulcl  15480  gzabssqcl  15483  4sqlem4a  15493  cshwshashlem2  15641  structcnvcnv  15706  structfun  15707  xpsff1o  16051  mre1cl  16077  drsbn0  16760  subgss  17418  symgfixelsi  17678  psgnunilem5  17737  pgpgrp  17832  slwsubg  17848  efgs1b  17972  efgsp1  17973  efgsres  17974  efgredeu  17988  efgred2  17989  efgcpbllemb  17991  srgmgp  18333  ringmgp  18376  irrednu  18528  lmodring  18694  lmodprop2d  18748  lssn0  18762  phlsrng  19795  ocvss  19833  obsss  19887  locfinbas  21135  fclsfil  21624  tmdtps  21690  tgptmd  21693  trgring  21784  tdrgdrng  21787  ngpms  22214  icopnfcnv  22549  xrhmeo  22553  oprpiece1res2  22559  phtpcer  22602  phtpcerOLD  22603  pcoval2  22624  pcoass  22632  clmsca  22673  cphsqrtcl  22792  bncms  22949  itg2ge0  23308  uc1pn0  23709  mon1pn0  23710  sinq12ge0  24064  cosq14gt0  24066  cosq14ge0  24067  sinord  24084  recosf1o  24085  resinf1o  24086  logrnaddcl  24125  logbcl  24305  relogbreexp  24313  atanf  24407  atanneg  24434  atancj  24437  efiatan  24439  atanlogaddlem  24440  atanlogadd  24441  atanlogsub  24443  efiatan2  24444  2efiatan  24445  tanatan  24446  dvatan  24462  areambl  24485  rlimcnp  24492  emgt0  24533  harmoniclbnd  24535  harmonicbnd4  24537  lgamgulmlem2  24556  gausslemma2dlem1a  24890  2sqlem2  24943  2sqlem3  24945  dchrvmasumlem2  24987  dchrvmasumiflem1  24990  logdivbnd  25045  pntpbnd2  25076  pnt  25103  brbtwn2  25585  ax5seglem3  25611  ax5seglem6  25614  axpaschlem  25620  axcontlem2  25645  axcontlem4  25647  eengbas  25661  ebtwntg  25662  ecgrtg  25663  elntg  25664  clwwisshclwwlem  26334  hst1a  28461  stge0  28467  sthil  28477  f1mptrn  28816  fsumrp0cl  29026  omndtos  29036  slmdsrg  29091  orngogrp  29132  psgnfzto1stlem  29181  elunitge0  29273  xrge0iifcnv  29307  xrge0iifcv  29308  xrge0iifiso  29309  rrextnlm  29375  rrextchr  29376  0elros  29560  0elsros  29567  voliune  29619  volfiniune  29620  bnj563  30067  bnj1212  30124  bnj1219  30125  bnj1366  30154  bnj1379  30155  bnj545  30219  bnj594  30236  bnj1118  30306  bnj1177  30328  bnj1190  30330  bnj1398  30356  bnj1417  30363  bnj1450  30372  bnj1312  30380  bnj1523  30393  msrval  30689  mclsppslem  30734  dfon2lem1  30932  dfrdg2  30945  cntotbnd  32765  heiborlem5  32784  heiborlem6  32785  atl0dm  33607  dalem-ccly  33989  elixpconstg  38294  stoweidlem60  38953  fourierdlem40  39040  fourierdlem78  39077  elfzo0l  40365  crctcsh1wlkn0lem4  41016  wwlkbp  41043  clwwisshclwwslem  41234  rngmgp  41668