Theorem simp1bi 1069

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 205	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp1d 1066	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 195   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  limord  5701  smores2  7338  smofvon2  7340  smofvon  7343  errel  7638  lincmb01cmp  12186  iccf1o  12187  elfznn0  12302  elfzouz  12343  ef01bndlem  14753  sin01bnd  14754  cos01bnd  14755  sin01gt0  14759  cos01gt0  14760  sin02gt0  14761  gzcn  15474  mresspw  16075  drsprs  16759  ipodrscl  16985  subgrcl  17422  pmtrfconj  17709  pgpprm  17831  slwprm  17847  efgsdmi  17968  efgsrel  17970  efgs1b  17972  efgsp1  17973  efgsres  17974  efgsfo  17975  efgredlema  17976  efgredlemf  17977  efgredlemd  17980  efgredlemc  17981  efgredlem  17983  efgrelexlemb  17986  efgcpbllemb  17991  srgcmn  18331  ringgrp  18375  irredcl  18527  lmodgrp  18693  lssss  18758  phllvec  19793  obsrcl  19886  locfintop  21134  fclstop  21625  tmdmnd  21689  tgpgrp  21692  trgtgp  21781  tdrgtrg  21786  ust0  21833  ngpgrp  22213  elii1  22542  elii2  22543  icopnfcnv  22549  icopnfhmeo  22550  iccpnfhmeo  22552  xrhmeo  22553  oprpiece1res1  22558  oprpiece1res2  22559  phtpcer  22602  phtpcerOLD  22603  pcoval2  22624  pcoass  22632  clmlmod  22675  cphphl  22779  cphnlm  22780  cphsca  22787  bnnvc  22945  uc1pcl  23707  mon1pcl  23708  sinq12ge0  24064  cosq14ge0  24067  cosord  24082  cos11  24083  recosf1o  24085  resinf1o  24086  efifo  24097  logrncn  24113  atanf  24407  atanneg  24434  efiatan  24439  atanlogaddlem  24440  atanlogadd  24441  atanlogsub  24443  efiatan2  24444  2efiatan  24445  tanatan  24446  areass  24486  dchrvmasumlem2  24987  dchrvmasumiflem1  24990  brbtwn2  25585  ax5seglem1  25608  ax5seglem2  25609  ax5seglem3  25611  ax5seglem5  25613  ax5seglem6  25614  ax5seglem9  25617  ax5seg  25618  axbtwnid  25619  axpaschlem  25620  axpasch  25621  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  2spotiundisj  26589  sticl  28458  hstcl  28460  omndmnd  29035  slmdcmn  29089  orngring  29131  elunitrn  29271  rrextnrg  29373  rrextdrg  29374  rossspw  29559  srossspw  29566  eulerpartlemd  29755  eulerpartlemf  29759  eulerpartlemgvv  29765  eulerpartlemgu  29766  eulerpartlemgh  29767  eulerpartlemgs2  29769  eulerpartlemn  29770  bnj564  30068  bnj1366  30154  bnj545  30219  bnj548  30221  bnj558  30226  bnj570  30229  bnj580  30237  bnj929  30260  bnj998  30280  bnj1006  30283  bnj1190  30330  bnj1523  30393  msrval  30689  mthmpps  30733  atllat  33605  stoweidlem60  38953  fourierdlem111  39110  clwwlkbp  41191  rngabl  41667