Theorem simp1bi 1157

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

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

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

This theorem is referenced by:  limord  6403  smores2  8320  smofvon2  8322  smofvon  8325  errel  8683  elunitrn  13468  lincmb01cmp  13496  iccf1o  13497  elfznn0  13622  elfzouz  13666  ef01bndlem  16199  sin01bnd  16200  cos01bnd  16201  sin01gt0  16205  cos01gt0  16206  sin02gt0  16207  gzcn  16951  mresspw  17603  drsprs  18318  ipodrscl  18553  subgrcl  19156  pmtrfconj  19489  pgpprm  19616  slwprm  19632  efgsdmi  19755  efgsrel  19757  efgs1b  19759  efgsp1  19760  efgsres  19761  efgsfo  19762  efgredlema  19763  efgredlemf  19764  efgredlemd  19767  efgredlemc  19768  efgredlem  19770  efgrelexlemb  19773  efgcpbllemb  19778  omndmnd  20149  rngabl  20184  srgcmn  20218  ringgrp  20267  irredcl  20452  subrngrcl  20580  sdrgrcl  20818  orngring  20891  lmodgrp  20914  lssss  20983  phllvec  21661  obsrcl  21755  locfintop  23561  fclstop  24051  tmdmnd  24115  tgpgrp  24118  trgtgp  24208  tdrgtrg  24213  ust0  24260  ngpgrp  24639  elii1  24977  elii2  24978  icopnfcnv  24984  icopnfhmeo  24985  iccpnfhmeo  24987  xrhmeo  24988  oprpiece1res2  24994  phtpcer  25037  pcoval2  25058  pcoass  25066  clmlmod  25109  cphphl  25213  cphnlm  25214  cphsca  25221  bnnvc  25382  uc1pcl  26184  mon1pcl  26185  sinq12ge0  26550  cosq14ge0  26553  cosq34lt1  26569  cosord  26573  cos11  26575  recosf1o  26577  resinf1o  26578  efifo  26589  logrncn  26604  atanf  26922  atanneg  26949  efiatan  26954  atanlogaddlem  26955  atanlogadd  26956  atanlogsub  26958  efiatan2  26959  2efiatan  26960  tanatan  26961  areass  27001  dchrvmasumlem2  27539  dchrvmasumiflem1  27542  brbtwn2  29052  ax5seglem1  29075  ax5seglem2  29076  ax5seglem3  29078  ax5seglem5  29080  ax5seglem6  29081  ax5seglem9  29084  ax5seg  29085  axbtwnid  29086  axpaschlem  29087  axpasch  29088  axcontlem2  29112  axcontlem4  29114  axcontlem7  29117  pthistrl  29869  clwwlkbp  30133  sticl  32364  hstcl  32366  slmdcmn  33346  rrextnrg  34259  rrextdrg  34260  rossspw  34427  srossspw  34434  eulerpartlemd  34624  eulerpartlemf  34628  eulerpartlemgvv  34634  eulerpartlemgu  34635  eulerpartlemgh  34636  eulerpartlemgs2  34638  eulerpartlemn  34639  bnj564  35004  bnj1366  35088  bnj545  35154  bnj548  35156  bnj558  35161  bnj570  35164  bnj580  35172  bnj929  35195  bnj998  35216  bnj1006  35219  bnj1190  35267  bnj1523  35330  msrval  35852  mthmpps  35896  eqvrelrefrel  39145  atllat  39888  stoweidlem60  46598  fourierdlem111  46755  modmknepk  47926  muldvdsfacgt  47944  prproropf1o  48077  gpgedgvtx1  48648  arweutermc  50115