Theorem simp1bi 1143

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

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

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 396  df-3an 1087

This theorem is referenced by:  limord  6424  smores2  8369  smofvon2  8371  smofvon  8374  errel  8728  elunitrn  13471  lincmb01cmp  13499  iccf1o  13500  elfznn0  13621  elfzouz  13663  ef01bndlem  16155  sin01bnd  16156  cos01bnd  16157  sin01gt0  16161  cos01gt0  16162  sin02gt0  16163  gzcn  16895  mresspw  17566  drsprs  18289  ipodrscl  18524  subgrcl  19080  pmtrfconj  19415  pgpprm  19542  slwprm  19558  efgsdmi  19681  efgsrel  19683  efgs1b  19685  efgsp1  19686  efgsres  19687  efgsfo  19688  efgredlema  19689  efgredlemf  19690  efgredlemd  19693  efgredlemc  19694  efgredlem  19696  efgrelexlemb  19699  efgcpbllemb  19704  rngabl  20089  srgcmn  20123  ringgrp  20172  irredcl  20357  subrngrcl  20482  sdrgrcl  20671  lmodgrp  20744  lssss  20814  phllvec  21555  obsrcl  21651  locfintop  23419  fclstop  23909  tmdmnd  23973  tgpgrp  23976  trgtgp  24066  tdrgtrg  24071  ust0  24118  ngpgrp  24502  elii1  24852  elii2  24853  icopnfcnv  24861  icopnfhmeo  24862  iccpnfhmeo  24864  xrhmeo  24865  oprpiece1res2  24871  phtpcer  24915  pcoval2  24937  pcoass  24945  clmlmod  24988  cphphl  25093  cphnlm  25094  cphsca  25101  bnnvc  25262  uc1pcl  26073  mon1pcl  26074  sinq12ge0  26437  cosq14ge0  26440  cosq34lt1  26455  cosord  26459  cos11  26461  recosf1o  26463  resinf1o  26464  efifo  26475  logrncn  26490  atanf  26806  atanneg  26833  efiatan  26838  atanlogaddlem  26839  atanlogadd  26840  atanlogsub  26842  efiatan2  26843  2efiatan  26844  tanatan  26845  areass  26885  dchrvmasumlem2  27425  dchrvmasumiflem1  27428  brbtwn2  28710  ax5seglem1  28733  ax5seglem2  28734  ax5seglem3  28736  ax5seglem5  28738  ax5seglem6  28739  ax5seglem9  28742  ax5seg  28743  axbtwnid  28744  axpaschlem  28745  axpasch  28746  axcontlem2  28770  axcontlem4  28772  axcontlem7  28775  pthistrl  29533  clwwlkbp  29789  sticl  32019  hstcl  32021  omndmnd  32779  slmdcmn  32907  orngring  33010  rrextnrg  33597  rrextdrg  33598  rossspw  33783  srossspw  33790  eulerpartlemd  33981  eulerpartlemf  33985  eulerpartlemgvv  33991  eulerpartlemgu  33992  eulerpartlemgh  33993  eulerpartlemgs2  33995  eulerpartlemn  33996  bnj564  34370  bnj1366  34455  bnj545  34521  bnj548  34523  bnj558  34528  bnj570  34531  bnj580  34539  bnj929  34562  bnj998  34583  bnj1006  34586  bnj1190  34634  bnj1523  34697  msrval  35143  mthmpps  35187  eqvrelrefrel  38065  atllat  38767  stoweidlem60  45439  fourierdlem111  45596  prproropf1o  46838