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 215	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp1d 1143	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:  limord  6425  smores2  8354  smofvon2  8356  smofvon  8359  errel  8712  elunitrn  13444  lincmb01cmp  13472  iccf1o  13473  elfznn0  13594  elfzouz  13636  ef01bndlem  16127  sin01bnd  16128  cos01bnd  16129  sin01gt0  16133  cos01gt0  16134  sin02gt0  16135  gzcn  16865  mresspw  17536  drsprs  18256  ipodrscl  18491  subgrcl  19011  pmtrfconj  19334  pgpprm  19461  slwprm  19477  efgsdmi  19600  efgsrel  19602  efgs1b  19604  efgsp1  19605  efgsres  19606  efgsfo  19607  efgredlema  19608  efgredlemf  19609  efgredlemd  19612  efgredlemc  19613  efgredlem  19615  efgrelexlemb  19618  efgcpbllemb  19623  srgcmn  20012  ringgrp  20061  irredcl  20238  sdrgrcl  20405  lmodgrp  20478  lssss  20547  phllvec  21182  obsrcl  21278  locfintop  23025  fclstop  23515  tmdmnd  23579  tgpgrp  23582  trgtgp  23672  tdrgtrg  23677  ust0  23724  ngpgrp  24108  elii1  24451  elii2  24452  icopnfcnv  24458  icopnfhmeo  24459  iccpnfhmeo  24461  xrhmeo  24462  oprpiece1res2  24468  phtpcer  24511  pcoval2  24532  pcoass  24540  clmlmod  24583  cphphl  24688  cphnlm  24689  cphsca  24696  bnnvc  24857  uc1pcl  25661  mon1pcl  25662  sinq12ge0  26018  cosq14ge0  26021  cosq34lt1  26036  cosord  26040  cos11  26042  recosf1o  26044  resinf1o  26045  efifo  26056  logrncn  26071  atanf  26385  atanneg  26412  efiatan  26417  atanlogaddlem  26418  atanlogadd  26419  atanlogsub  26421  efiatan2  26422  2efiatan  26423  tanatan  26424  areass  26464  dchrvmasumlem2  27001  dchrvmasumiflem1  27004  brbtwn2  28163  ax5seglem1  28186  ax5seglem2  28187  ax5seglem3  28189  ax5seglem5  28191  ax5seglem6  28192  ax5seglem9  28195  ax5seg  28196  axbtwnid  28197  axpaschlem  28198  axpasch  28199  axcontlem2  28223  axcontlem4  28225  axcontlem7  28228  pthistrl  28982  clwwlkbp  29238  sticl  31468  hstcl  31470  omndmnd  32222  slmdcmn  32350  orngring  32418  rrextnrg  32981  rrextdrg  32982  rossspw  33167  srossspw  33174  eulerpartlemd  33365  eulerpartlemf  33369  eulerpartlemgvv  33375  eulerpartlemgu  33376  eulerpartlemgh  33377  eulerpartlemgs2  33379  eulerpartlemn  33380  bnj564  33755  bnj1366  33840  bnj545  33906  bnj548  33908  bnj558  33913  bnj570  33916  bnj580  33924  bnj929  33947  bnj998  33968  bnj1006  33971  bnj1190  34019  bnj1523  34082  msrval  34529  mthmpps  34573  eqvrelrefrel  37468  atllat  38170  stoweidlem60  44776  fourierdlem111  44933  prproropf1o  46175  rngabl  46651  subrngrcl  46730