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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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

This theorem is referenced by:  limord  6386  smores2  8296  smofvon2  8298  smofvon  8301  errel  8655  elunitrn  13395  lincmb01cmp  13423  iccf1o  13424  elfznn0  13548  elfzouz  13591  ef01bndlem  16121  sin01bnd  16122  cos01bnd  16123  sin01gt0  16127  cos01gt0  16128  sin02gt0  16129  gzcn  16872  mresspw  17523  drsprs  18238  ipodrscl  18473  subgrcl  19073  pmtrfconj  19407  pgpprm  19534  slwprm  19550  efgsdmi  19673  efgsrel  19675  efgs1b  19677  efgsp1  19678  efgsres  19679  efgsfo  19680  efgredlema  19681  efgredlemf  19682  efgredlemd  19685  efgredlemc  19686  efgredlem  19688  efgrelexlemb  19691  efgcpbllemb  19696  omndmnd  20067  rngabl  20102  srgcmn  20136  ringgrp  20185  irredcl  20372  subrngrcl  20496  sdrgrcl  20734  orngring  20807  lmodgrp  20830  lssss  20899  phllvec  21596  obsrcl  21690  locfintop  23477  fclstop  23967  tmdmnd  24031  tgpgrp  24034  trgtgp  24124  tdrgtrg  24129  ust0  24176  ngpgrp  24555  elii1  24899  elii2  24900  icopnfcnv  24908  icopnfhmeo  24909  iccpnfhmeo  24911  xrhmeo  24912  oprpiece1res2  24918  phtpcer  24962  pcoval2  24984  pcoass  24992  clmlmod  25035  cphphl  25139  cphnlm  25140  cphsca  25147  bnnvc  25308  uc1pcl  26117  mon1pcl  26118  sinq12ge0  26485  cosq14ge0  26488  cosq34lt1  26504  cosord  26508  cos11  26510  recosf1o  26512  resinf1o  26513  efifo  26524  logrncn  26539  atanf  26858  atanneg  26885  efiatan  26890  atanlogaddlem  26891  atanlogadd  26892  atanlogsub  26894  efiatan2  26895  2efiatan  26896  tanatan  26897  areass  26937  dchrvmasumlem2  27477  dchrvmasumiflem1  27480  brbtwn2  28990  ax5seglem1  29013  ax5seglem2  29014  ax5seglem3  29016  ax5seglem5  29018  ax5seglem6  29019  ax5seglem9  29022  ax5seg  29023  axbtwnid  29024  axpaschlem  29025  axpasch  29026  axcontlem2  29050  axcontlem4  29052  axcontlem7  29055  pthistrl  29808  clwwlkbp  30072  sticl  32302  hstcl  32304  slmdcmn  33298  rrextnrg  34178  rrextdrg  34179  rossspw  34346  srossspw  34353  eulerpartlemd  34543  eulerpartlemf  34547  eulerpartlemgvv  34553  eulerpartlemgu  34554  eulerpartlemgh  34555  eulerpartlemgs2  34557  eulerpartlemn  34558  bnj564  34920  bnj1366  35004  bnj545  35070  bnj548  35072  bnj558  35077  bnj570  35080  bnj580  35088  bnj929  35111  bnj998  35132  bnj1006  35135  bnj1190  35183  bnj1523  35246  msrval  35751  mthmpps  35795  eqvrelrefrel  38927  atllat  39670  stoweidlem60  46412  fourierdlem111  46569  modmknepk  47716  prproropf1o  47861  gpgedgvtx1  48416  arweutermc  49883