Theorem simp1bi 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
simp1bi	⊢ (𝜑 → 𝜓)

Proof of Theorem simp1bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
2	1	biimpi 216	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp1d 1143	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  limord  6378  smores2  8287  smofvon2  8289  smofvon  8292  errel  8646  elunitrn  13411  lincmb01cmp  13439  iccf1o  13440  elfznn0  13565  elfzouz  13609  ef01bndlem  16142  sin01bnd  16143  cos01bnd  16144  sin01gt0  16148  cos01gt0  16149  sin02gt0  16150  gzcn  16894  mresspw  17545  drsprs  18260  ipodrscl  18495  subgrcl  19098  pmtrfconj  19432  pgpprm  19559  slwprm  19575  efgsdmi  19698  efgsrel  19700  efgs1b  19702  efgsp1  19703  efgsres  19704  efgsfo  19705  efgredlema  19706  efgredlemf  19707  efgredlemd  19710  efgredlemc  19711  efgredlem  19713  efgrelexlemb  19716  efgcpbllemb  19721  omndmnd  20092  rngabl  20127  srgcmn  20161  ringgrp  20210  irredcl  20395  subrngrcl  20519  sdrgrcl  20757  orngring  20830  lmodgrp  20853  lssss  20922  phllvec  21619  obsrcl  21713  locfintop  23496  fclstop  23986  tmdmnd  24050  tgpgrp  24053  trgtgp  24143  tdrgtrg  24148  ust0  24195  ngpgrp  24574  elii1  24912  elii2  24913  icopnfcnv  24919  icopnfhmeo  24920  iccpnfhmeo  24922  xrhmeo  24923  oprpiece1res2  24929  phtpcer  24972  pcoval2  24993  pcoass  25001  clmlmod  25044  cphphl  25148  cphnlm  25149  cphsca  25156  bnnvc  25317  uc1pcl  26119  mon1pcl  26120  sinq12ge0  26485  cosq14ge0  26488  cosq34lt1  26504  cosord  26508  cos11  26510  recosf1o  26512  resinf1o  26513  efifo  26524  logrncn  26539  atanf  26857  atanneg  26884  efiatan  26889  atanlogaddlem  26890  atanlogadd  26891  atanlogsub  26893  efiatan2  26894  2efiatan  26895  tanatan  26896  areass  26936  dchrvmasumlem2  27475  dchrvmasumiflem1  27478  brbtwn2  28988  ax5seglem1  29011  ax5seglem2  29012  ax5seglem3  29014  ax5seglem5  29016  ax5seglem6  29017  ax5seglem9  29020  ax5seg  29021  axbtwnid  29022  axpaschlem  29023  axpasch  29024  axcontlem2  29048  axcontlem4  29050  axcontlem7  29053  pthistrl  29806  clwwlkbp  30070  sticl  32301  hstcl  32303  slmdcmn  33281  rrextnrg  34161  rrextdrg  34162  rossspw  34329  srossspw  34336  eulerpartlemd  34526  eulerpartlemf  34530  eulerpartlemgvv  34536  eulerpartlemgu  34537  eulerpartlemgh  34538  eulerpartlemgs2  34540  eulerpartlemn  34541  bnj564  34903  bnj1366  34987  bnj545  35053  bnj548  35055  bnj558  35060  bnj570  35063  bnj580  35071  bnj929  35094  bnj998  35115  bnj1006  35118  bnj1190  35166  bnj1523  35229  msrval  35736  mthmpps  35780  eqvrelrefrel  39017  atllat  39760  stoweidlem60  46506  fourierdlem111  46663  modmknepk  47828  muldvdsfacgt  47846  prproropf1o  47979  gpgedgvtx1  48550  arweutermc  50017