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

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

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 397  df-3an 1089

This theorem is referenced by:  smodm  8353  erdm  8715  ixpfn  8899  winafp  10694  inar1  10772  inatsk  10775  tskuni  10780  grur1  10817  supmullem1  12186  supmullem2  12187  supmul  12188  eluzelz  12834  elfz3nn0  13597  elfzo0l  13724  ico01fl0  13786  addmodlteq  13913  cshco  14789  swrds2  14893  ef01bndlem  16129  sin01bnd  16130  cos01bnd  16131  sin01gt0  16135  bitsss  16369  smueqlem  16433  gznegcl  16870  gzcjcl  16871  gzaddcl  16872  gzmulcl  16873  gzabssqcl  16876  4sqlem4a  16886  cshwshashlem2  17032  structn0fun  17086  xpsff1o  17515  mre1cl  17540  drsbn0  18259  subgss  19009  symgfixelsi  19305  psgnunilem5  19364  pgpgrp  19464  slwsubg  19480  efgs1b  19606  efgsp1  19607  efgsres  19608  efgredeu  19622  efgred2  19623  efgcpbllemb  19625  srgmgp  20016  ringmgp  20064  irrednu  20243  sdrgsubrg  20411  fldsdrgfld  20418  sdrgint  20424  primefld  20425  primefld0cl  20426  primefld1cl  20427  lmodring  20483  lmodprop2d  20539  lssn0  20556  phlsrng  21190  ocvss  21229  obsss  21285  locfinbas  23033  fclsfil  23521  tmdtps  23587  tgptmd  23590  trgring  23682  tdrgdrng  23685  ngpms  24116  icopnfcnv  24465  xrhmeo  24469  oprpiece1res2  24475  phtpcer  24518  pcoval2  24539  pcoass  24547  clmsca  24588  cphsqrtcl  24708  bncms  24868  itg2ge0  25260  uc1pn0  25670  mon1pn0  25671  sinq12ge0  26025  cosq14gt0  26027  cosq14ge0  26028  cos02pilt1  26042  cosq34lt1  26043  sinord  26050  recosf1o  26051  resinf1o  26052  logrnaddcl  26090  logbcl  26279  relogbreexp  26287  atanf  26392  atanneg  26419  atancj  26422  efiatan  26424  atanlogaddlem  26425  atanlogadd  26426  atanlogsub  26428  efiatan2  26429  2efiatan  26430  tanatan  26431  dvatan  26447  areambl  26470  rlimcnp  26477  emgt0  26518  harmoniclbnd  26520  harmonicbnd4  26522  lgamgulmlem2  26541  gausslemma2dlem1a  26875  2sqlem2  26928  2sqlem3  26930  dchrvmasumlem2  27008  dchrvmasumiflem1  27011  logdivbnd  27066  pntpbnd2  27097  pnt  27124  brbtwn2  28201  ax5seglem3  28227  ax5seglem6  28230  axpaschlem  28236  axcontlem2  28261  axcontlem4  28263  crctcshwlkn0lem4  29105  wwlkbp  29133  clwwisshclwwslem  29305  hst1a  31509  stge0  31515  sthil  31525  neldifpr1  31808  f1mptrn  31897  cshwrnid  32163  fsumrp0cl  32234  omndtos  32264  psgnfzto1stlem  32300  slmdsrg  32393  primefldchr  32440  fldgensdrg  32445  primefldgen1  32452  orngogrp  32460  elunitge0  32948  xrge0iifcnv  32982  xrge0iifcv  32983  xrge0iifiso  32984  rrextnlm  33052  rrextchr  33053  0elros  33237  0elsros  33244  voliune  33296  volfiniune  33297  bnj563  33823  bnj1212  33879  bnj1219  33880  bnj1366  33909  bnj1379  33910  bnj545  33975  bnj594  33992  bnj1118  34064  bnj1177  34086  bnj1190  34088  bnj1398  34114  bnj1417  34121  bnj1450  34130  bnj1312  34138  bnj1523  34151  pthhashvtx  34187  msrval  34598  mclsppslem  34643  dfon2lem1  34824  dfrdg2  34836  cntotbnd  36750  heiborlem5  36769  heiborlem6  36770  eqvrelsymrel  37555  atl0dm  38258  dalem-ccly  38642  stoweidlem60  44855  fourierdlem40  44942  fourierdlem78  44979  rngmgp  46731  ackval40  47457