Theorem simp1bi 1142

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 1139	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  limord  6438  smores2  8388  smofvon2  8390  smofvon  8393  errel  8747  elunitrn  13502  lincmb01cmp  13530  iccf1o  13531  elfznn0  13652  elfzouz  13694  ef01bndlem  16199  sin01bnd  16200  cos01bnd  16201  sin01gt0  16205  cos01gt0  16206  sin02gt0  16207  gzcn  16947  mresspw  17618  drsprs  18341  ipodrscl  18576  subgrcl  19139  pmtrfconj  19476  pgpprm  19603  slwprm  19619  efgsdmi  19742  efgsrel  19744  efgs1b  19746  efgsp1  19747  efgsres  19748  efgsfo  19749  efgredlema  19750  efgredlemf  19751  efgredlemd  19754  efgredlemc  19755  efgredlem  19757  efgrelexlemb  19760  efgcpbllemb  19765  rngabl  20150  srgcmn  20184  ringgrp  20233  irredcl  20418  subrngrcl  20545  sdrgrcl  20780  lmodgrp  20855  lssss  20925  phllvec  21638  obsrcl  21734  locfintop  23516  fclstop  24006  tmdmnd  24070  tgpgrp  24073  trgtgp  24163  tdrgtrg  24168  ust0  24215  ngpgrp  24599  elii1  24949  elii2  24950  icopnfcnv  24958  icopnfhmeo  24959  iccpnfhmeo  24961  xrhmeo  24962  oprpiece1res2  24968  phtpcer  25012  pcoval2  25034  pcoass  25042  clmlmod  25085  cphphl  25190  cphnlm  25191  cphsca  25198  bnnvc  25359  uc1pcl  26168  mon1pcl  26169  sinq12ge0  26533  cosq14ge0  26536  cosq34lt1  26551  cosord  26555  cos11  26557  recosf1o  26559  resinf1o  26560  efifo  26571  logrncn  26586  atanf  26905  atanneg  26932  efiatan  26937  atanlogaddlem  26938  atanlogadd  26939  atanlogsub  26941  efiatan2  26942  2efiatan  26943  tanatan  26944  areass  26984  dchrvmasumlem2  27524  dchrvmasumiflem1  27527  brbtwn2  28881  ax5seglem1  28904  ax5seglem2  28905  ax5seglem3  28907  ax5seglem5  28909  ax5seglem6  28910  ax5seglem9  28913  ax5seg  28914  axbtwnid  28915  axpaschlem  28916  axpasch  28917  axcontlem2  28941  axcontlem4  28943  axcontlem7  28946  pthistrl  29704  clwwlkbp  29960  sticl  32190  hstcl  32192  omndmnd  32999  slmdcmn  33129  orngring  33240  rrextnrg  33892  rrextdrg  33893  rossspw  34078  srossspw  34085  eulerpartlemd  34276  eulerpartlemf  34280  eulerpartlemgvv  34286  eulerpartlemgu  34287  eulerpartlemgh  34288  eulerpartlemgs2  34290  eulerpartlemn  34291  bnj564  34665  bnj1366  34750  bnj545  34816  bnj548  34818  bnj558  34823  bnj570  34826  bnj580  34834  bnj929  34857  bnj998  34878  bnj1006  34881  bnj1190  34929  bnj1523  34992  msrval  35451  mthmpps  35495  eqvrelrefrel  38381  atllat  39083  stoweidlem60  45792  fourierdlem111  45949  prproropf1o  47190