Theorem simp2bi 1148

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

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

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 400  df-3an 1091

This theorem is referenced by:  smodm  8088  erdm  8401  ixpfn  8584  winafp  10311  inar1  10389  inatsk  10392  tskuni  10397  grur1  10434  supmullem1  11802  supmullem2  11803  supmul  11804  eluzelz  12448  elfz3nn0  13206  elfzo0l  13332  ico01fl0  13394  addmodlteq  13519  cshco  14401  swrds2  14505  ef01bndlem  15745  sin01bnd  15746  cos01bnd  15747  sin01gt0  15751  bitsss  15985  smueqlem  16049  gznegcl  16488  gzcjcl  16489  gzaddcl  16490  gzmulcl  16491  gzabssqcl  16494  4sqlem4a  16504  cshwshashlem2  16650  structn0fun  16704  xpsff1o  17072  mre1cl  17097  drsbn0  17811  subgss  18544  symgfixelsi  18827  psgnunilem5  18886  pgpgrp  18983  slwsubg  18999  efgs1b  19126  efgsp1  19127  efgsres  19128  efgredeu  19142  efgred2  19143  efgcpbllemb  19145  srgmgp  19525  ringmgp  19568  irrednu  19723  sdrgint  19848  primefld  19849  primefld0cl  19850  primefld1cl  19851  lmodring  19907  lmodprop2d  19961  lssn0  19977  phlsrng  20593  ocvss  20632  obsss  20686  locfinbas  22419  fclsfil  22907  tmdtps  22973  tgptmd  22976  trgring  23068  tdrgdrng  23071  ngpms  23498  icopnfcnv  23839  xrhmeo  23843  oprpiece1res2  23849  phtpcer  23892  pcoval2  23913  pcoass  23921  clmsca  23962  cphsqrtcl  24081  bncms  24241  itg2ge0  24633  uc1pn0  25043  mon1pn0  25044  sinq12ge0  25398  cosq14gt0  25400  cosq14ge0  25401  cos02pilt1  25415  cosq34lt1  25416  sinord  25423  recosf1o  25424  resinf1o  25425  logrnaddcl  25463  logbcl  25650  relogbreexp  25658  atanf  25763  atanneg  25790  atancj  25793  efiatan  25795  atanlogaddlem  25796  atanlogadd  25797  atanlogsub  25799  efiatan2  25800  2efiatan  25801  tanatan  25802  dvatan  25818  areambl  25841  rlimcnp  25848  emgt0  25889  harmoniclbnd  25891  harmonicbnd4  25893  lgamgulmlem2  25912  gausslemma2dlem1a  26246  2sqlem2  26299  2sqlem3  26301  dchrvmasumlem2  26379  dchrvmasumiflem1  26382  logdivbnd  26437  pntpbnd2  26468  pnt  26495  brbtwn2  26996  ax5seglem3  27022  ax5seglem6  27025  axpaschlem  27031  axcontlem2  27056  axcontlem4  27058  crctcshwlkn0lem4  27897  wwlkbp  27925  clwwisshclwwslem  28097  hst1a  30299  stge0  30305  sthil  30315  neldifpr1  30600  f1mptrn  30689  cshwrnid  30953  fsumrp0cl  31023  omndtos  31050  psgnfzto1stlem  31086  slmdsrg  31179  primefldchr  31212  orngogrp  31219  elunitge0  31563  xrge0iifcnv  31597  xrge0iifcv  31598  xrge0iifiso  31599  rrextnlm  31665  rrextchr  31666  0elros  31850  0elsros  31857  voliune  31909  volfiniune  31910  bnj563  32435  bnj1212  32492  bnj1219  32493  bnj1366  32522  bnj1379  32523  bnj545  32588  bnj594  32605  bnj1118  32677  bnj1177  32699  bnj1190  32701  bnj1398  32727  bnj1417  32734  bnj1450  32743  bnj1312  32751  bnj1523  32764  pthhashvtx  32802  msrval  33213  mclsppslem  33258  dfon2lem1  33478  dfrdg2  33490  cntotbnd  35691  heiborlem5  35710  heiborlem6  35711  eqvrelsymrel  36449  atl0dm  37053  dalem-ccly  37436  stoweidlem60  43276  fourierdlem40  43363  fourierdlem78  43400  rngmgp  45109  ackval40  45712