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  28194  ax5seglem1  28217  ax5seglem2  28218  ax5seglem3  28220  ax5seglem5  28222  ax5seglem6  28223  ax5seglem9  28226  ax5seg  28227  axbtwnid  28228  axpaschlem  28229  axpasch  28230  axcontlem2  28254  axcontlem4  28256  axcontlem7  28259  pthistrl  29013  clwwlkbp  29269  sticl  31499  hstcl  31501  omndmnd  32253  slmdcmn  32381  orngring  32449  rrextnrg  33012  rrextdrg  33013  rossspw  33198  srossspw  33205  eulerpartlemd  33396  eulerpartlemf  33400  eulerpartlemgvv  33406  eulerpartlemgu  33407  eulerpartlemgh  33408  eulerpartlemgs2  33410  eulerpartlemn  33411  bnj564  33786  bnj1366  33871  bnj545  33937  bnj548  33939  bnj558  33944  bnj570  33947  bnj580  33955  bnj929  33978  bnj998  33999  bnj1006  34002  bnj1190  34050  bnj1523  34113  msrval  34560  mthmpps  34604  eqvrelrefrel  37516  atllat  38218  stoweidlem60  44824  fourierdlem111  44981  prproropf1o  46223  rngabl  46699  subrngrcl  46778