Theorem simp1bi 1141

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 218	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp1d 1138	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  limord  6253  smores2  7994  smofvon2  7996  smofvon  7999  errel  8301  lincmb01cmp  12884  iccf1o  12885  elfznn0  13003  elfzouz  13045  ef01bndlem  15540  sin01bnd  15541  cos01bnd  15542  sin01gt0  15546  cos01gt0  15547  sin02gt0  15548  gzcn  16271  mresspw  16866  drsprs  17549  ipodrscl  17775  subgrcl  18287  pmtrfconj  18597  pgpprm  18721  slwprm  18737  efgsdmi  18861  efgsrel  18863  efgs1b  18865  efgsp1  18866  efgsres  18867  efgsfo  18868  efgredlema  18869  efgredlemf  18870  efgredlemd  18873  efgredlemc  18874  efgredlem  18876  efgrelexlemb  18879  efgcpbllemb  18884  srgcmn  19261  ringgrp  19305  irredcl  19457  lmodgrp  19644  lssss  19711  phllvec  20776  obsrcl  20870  locfintop  22132  fclstop  22622  tmdmnd  22686  tgpgrp  22689  trgtgp  22779  tdrgtrg  22784  ust0  22831  ngpgrp  23211  elii1  23542  elii2  23543  icopnfcnv  23549  icopnfhmeo  23550  iccpnfhmeo  23552  xrhmeo  23553  oprpiece1res2  23559  phtpcer  23602  pcoval2  23623  pcoass  23631  clmlmod  23674  cphphl  23778  cphnlm  23779  cphsca  23786  bnnvc  23946  uc1pcl  24740  mon1pcl  24741  sinq12ge0  25097  cosq14ge0  25100  cosq34lt1  25115  cosord  25119  cos11  25120  recosf1o  25122  resinf1o  25123  efifo  25134  logrncn  25149  atanf  25461  atanneg  25488  efiatan  25493  atanlogaddlem  25494  atanlogadd  25495  atanlogsub  25497  efiatan2  25498  2efiatan  25499  tanatan  25500  areass  25540  dchrvmasumlem2  26077  dchrvmasumiflem1  26080  brbtwn2  26694  ax5seglem1  26717  ax5seglem2  26718  ax5seglem3  26720  ax5seglem5  26722  ax5seglem6  26723  ax5seglem9  26726  ax5seg  26727  axbtwnid  26728  axpaschlem  26729  axpasch  26730  axcontlem2  26754  axcontlem4  26756  axcontlem7  26759  pthistrl  27509  clwwlkbp  27766  sticl  29995  hstcl  29997  omndmnd  30709  slmdcmn  30837  orngring  30877  elunitrn  31144  rrextnrg  31246  rrextdrg  31247  rossspw  31432  srossspw  31439  eulerpartlemd  31628  eulerpartlemf  31632  eulerpartlemgvv  31638  eulerpartlemgu  31639  eulerpartlemgh  31640  eulerpartlemgs2  31642  eulerpartlemn  31643  bnj564  32019  bnj1366  32105  bnj545  32171  bnj548  32173  bnj558  32178  bnj570  32181  bnj580  32189  bnj929  32212  bnj998  32233  bnj1006  32236  bnj1190  32284  bnj1523  32347  msrval  32789  mthmpps  32833  eqvrelrefrel  35837  atllat  36440  stoweidlem60  42352  fourierdlem111  42509  prproropf1o  43676  rngabl  44155