Theorem simp2bi 1152

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ w3a 1092

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

This theorem is referenced by:  0ellim  6381  smodm  8288  erdm  8651  ixpfn  8848  winafp  10618  inar1  10696  inatsk  10699  tskuni  10704  grur1  10741  supmullem1  12124  supmullem2  12125  supmul  12126  eluzelz  12796  elfz3nn0  13573  elfzo0l  13709  ico01fl0  13776  addmodlteq  13906  cshco  14796  swrds2  14900  ef01bndlem  16149  sin01bnd  16150  cos01bnd  16151  sin01gt0  16155  bitsss  16393  smueqlem  16457  gznegcl  16904  gzcjcl  16905  gzaddcl  16906  gzmulcl  16907  gzabssqcl  16910  4sqlem4a  16920  cshwshashlem2  17065  structn0fun  17119  xpsff1o  17529  mre1cl  17554  drsbn0  18268  subgss  19101  symgfixelsi  19408  psgnunilem5  19467  pgpgrp  19567  slwsubg  19583  efgs1b  19709  efgsp1  19710  efgsres  19711  efgredeu  19725  efgred2  19726  efgcpbllemb  19728  omndtos  20100  rngmgp  20135  srgmgp  20170  ringmgp  20218  irrednu  20403  sdrgsubrg  20770  fldsdrgfld  20777  sdrgint  20783  primefld  20784  primefld0cl  20785  primefld1cl  20786  orngogrp  20842  lmodring  20865  lmodprop2d  20921  lssn0  20937  phlsrng  21613  ocvss  21652  obsss  21706  locfinbas  23512  fclsfil  24000  tmdtps  24066  tgptmd  24069  trgring  24161  tdrgdrng  24164  ngpms  24590  icopnfcnv  24934  xrhmeo  24938  oprpiece1res2  24944  phtpcer  24987  pcoval2  25008  pcoass  25016  clmsca  25057  cphsqrtcl  25176  bncms  25336  itg2ge0  25727  uc1pn0  26136  mon1pn0  26137  sinq12ge0  26497  cosq14gt0  26499  cosq14ge0  26500  cos02pilt1  26515  cosq34lt1  26516  sinord  26523  recosf1o  26524  resinf1o  26525  logrnaddcl  26563  logbcl  26756  relogbreexp  26764  atanf  26869  atanneg  26896  atancj  26899  efiatan  26901  atanlogaddlem  26902  atanlogadd  26903  atanlogsub  26905  efiatan2  26906  2efiatan  26907  tanatan  26908  dvatan  26924  areambl  26947  rlimcnp  26954  emgt0  26995  harmoniclbnd  26997  harmonicbnd4  26999  lgamgulmlem2  27018  gausslemma2dlem1a  27353  2sqlem2  27406  2sqlem3  27408  dchrvmasumlem2  27486  dchrvmasumiflem1  27489  logdivbnd  27544  pntpbnd2  27575  pnt  27602  brbtwn2  28999  ax5seglem3  29025  ax5seglem6  29028  axpaschlem  29034  axcontlem2  29059  axcontlem4  29061  crctcshwlkn0lem4  29906  wwlkbp  29934  clwwisshclwwslem  30109  hst1a  32314  stge0  32320  sthil  32330  neldifpr1  32628  f1mptrn  32734  cshwrnid  33047  fsumrp0cl  33107  fzo0pmtrlast  33180  wrdpmtrlast  33181  psgnfzto1stlem  33188  slmdsrg  33295  primefldchr  33392  fldgensdrg  33405  primefldgen1  33412  1arithidomlem1  33625  1arithidomlem2  33626  1arithidom  33627  elunitge0  34090  xrge0iifcnv  34124  xrge0iifcv  34125  xrge0iifiso  34126  rrextnlm  34194  rrextchr  34195  0elros  34361  0elsros  34368  voliune  34420  volfiniune  34421  bnj563  34933  bnj1212  34988  bnj1219  34989  bnj1366  35018  bnj1379  35019  bnj545  35084  bnj594  35101  bnj1118  35173  bnj1177  35195  bnj1190  35197  bnj1398  35223  bnj1417  35230  bnj1450  35239  bnj1312  35247  bnj1523  35260  pthhashvtx  35363  msrval  35773  mclsppslem  35818  dfon2lem1  36016  dfrdg2  36028  cntotbnd  38170  heiborlem5  38189  heiborlem6  38190  eqvrelsymrel  39057  atl0dm  39801  dalem-ccly  40184  stoweidlem60  46510  fourierdlem40  46597  fourierdlem78  46634  upgrimpthslem1  48405  usgrgrtrirex  48448  ackval40  49191