Theorem simp2bi 1147

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

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

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 398  df-3an 1090

This theorem is referenced by:  smodm  8346  erdm  8709  ixpfn  8893  winafp  10688  inar1  10766  inatsk  10769  tskuni  10774  grur1  10811  supmullem1  12180  supmullem2  12181  supmul  12182  eluzelz  12828  elfz3nn0  13591  elfzo0l  13718  ico01fl0  13780  addmodlteq  13907  cshco  14783  swrds2  14887  ef01bndlem  16123  sin01bnd  16124  cos01bnd  16125  sin01gt0  16129  bitsss  16363  smueqlem  16427  gznegcl  16864  gzcjcl  16865  gzaddcl  16866  gzmulcl  16867  gzabssqcl  16870  4sqlem4a  16880  cshwshashlem2  17026  structn0fun  17080  xpsff1o  17509  mre1cl  17534  drsbn0  18253  subgss  19001  symgfixelsi  19296  psgnunilem5  19355  pgpgrp  19455  slwsubg  19471  efgs1b  19597  efgsp1  19598  efgsres  19599  efgredeu  19613  efgred2  19614  efgcpbllemb  19616  srgmgp  20005  ringmgp  20053  irrednu  20228  sdrgsubrg  20395  fldsdrgfld  20402  sdrgint  20408  primefld  20409  primefld0cl  20410  primefld1cl  20411  lmodring  20467  lmodprop2d  20522  lssn0  20539  phlsrng  21168  ocvss  21207  obsss  21263  locfinbas  23008  fclsfil  23496  tmdtps  23562  tgptmd  23565  trgring  23657  tdrgdrng  23660  ngpms  24091  icopnfcnv  24440  xrhmeo  24444  oprpiece1res2  24450  phtpcer  24493  pcoval2  24514  pcoass  24522  clmsca  24563  cphsqrtcl  24683  bncms  24843  itg2ge0  25235  uc1pn0  25645  mon1pn0  25646  sinq12ge0  26000  cosq14gt0  26002  cosq14ge0  26003  cos02pilt1  26017  cosq34lt1  26018  sinord  26025  recosf1o  26026  resinf1o  26027  logrnaddcl  26065  logbcl  26252  relogbreexp  26260  atanf  26365  atanneg  26392  atancj  26395  efiatan  26397  atanlogaddlem  26398  atanlogadd  26399  atanlogsub  26401  efiatan2  26402  2efiatan  26403  tanatan  26404  dvatan  26420  areambl  26443  rlimcnp  26450  emgt0  26491  harmoniclbnd  26493  harmonicbnd4  26495  lgamgulmlem2  26514  gausslemma2dlem1a  26848  2sqlem2  26901  2sqlem3  26903  dchrvmasumlem2  26981  dchrvmasumiflem1  26984  logdivbnd  27039  pntpbnd2  27070  pnt  27097  brbtwn2  28143  ax5seglem3  28169  ax5seglem6  28172  axpaschlem  28178  axcontlem2  28203  axcontlem4  28205  crctcshwlkn0lem4  29047  wwlkbp  29075  clwwisshclwwslem  29247  hst1a  31449  stge0  31455  sthil  31465  neldifpr1  31748  f1mptrn  31837  cshwrnid  32103  fsumrp0cl  32174  omndtos  32201  psgnfzto1stlem  32237  slmdsrg  32330  primefldchr  32368  fldgensdrg  32373  primefldgen1  32380  orngogrp  32388  elunitge0  32817  xrge0iifcnv  32851  xrge0iifcv  32852  xrge0iifiso  32853  rrextnlm  32921  rrextchr  32922  0elros  33106  0elsros  33113  voliune  33165  volfiniune  33166  bnj563  33692  bnj1212  33748  bnj1219  33749  bnj1366  33778  bnj1379  33779  bnj545  33844  bnj594  33861  bnj1118  33933  bnj1177  33955  bnj1190  33957  bnj1398  33983  bnj1417  33990  bnj1450  33999  bnj1312  34007  bnj1523  34020  pthhashvtx  34056  msrval  34467  mclsppslem  34512  dfon2lem1  34693  dfrdg2  34705  cntotbnd  36602  heiborlem5  36621  heiborlem6  36622  eqvrelsymrel  37407  atl0dm  38110  dalem-ccly  38494  stoweidlem60  44711  fourierdlem40  44798  fourierdlem78  44835  rngmgp  46587  ackval40  47281