Theorem simp1bi 1145

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

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

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 1088

This theorem is referenced by:  limord  6378  smores2  8286  smofvon2  8288  smofvon  8291  errel  8644  elunitrn  13383  lincmb01cmp  13411  iccf1o  13412  elfznn0  13536  elfzouz  13579  ef01bndlem  16109  sin01bnd  16110  cos01bnd  16111  sin01gt0  16115  cos01gt0  16116  sin02gt0  16117  gzcn  16860  mresspw  17511  drsprs  18226  ipodrscl  18461  subgrcl  19061  pmtrfconj  19395  pgpprm  19522  slwprm  19538  efgsdmi  19661  efgsrel  19663  efgs1b  19665  efgsp1  19666  efgsres  19667  efgsfo  19668  efgredlema  19669  efgredlemf  19670  efgredlemd  19673  efgredlemc  19674  efgredlem  19676  efgrelexlemb  19679  efgcpbllemb  19684  omndmnd  20055  rngabl  20090  srgcmn  20124  ringgrp  20173  irredcl  20360  subrngrcl  20484  sdrgrcl  20722  orngring  20795  lmodgrp  20818  lssss  20887  phllvec  21584  obsrcl  21678  locfintop  23465  fclstop  23955  tmdmnd  24019  tgpgrp  24022  trgtgp  24112  tdrgtrg  24117  ust0  24164  ngpgrp  24543  elii1  24887  elii2  24888  icopnfcnv  24896  icopnfhmeo  24897  iccpnfhmeo  24899  xrhmeo  24900  oprpiece1res2  24906  phtpcer  24950  pcoval2  24972  pcoass  24980  clmlmod  25023  cphphl  25127  cphnlm  25128  cphsca  25135  bnnvc  25296  uc1pcl  26105  mon1pcl  26106  sinq12ge0  26473  cosq14ge0  26476  cosq34lt1  26492  cosord  26496  cos11  26498  recosf1o  26500  resinf1o  26501  efifo  26512  logrncn  26527  atanf  26846  atanneg  26873  efiatan  26878  atanlogaddlem  26879  atanlogadd  26880  atanlogsub  26882  efiatan2  26883  2efiatan  26884  tanatan  26885  areass  26925  dchrvmasumlem2  27465  dchrvmasumiflem1  27468  brbtwn2  28978  ax5seglem1  29001  ax5seglem2  29002  ax5seglem3  29004  ax5seglem5  29006  ax5seglem6  29007  ax5seglem9  29010  ax5seg  29011  axbtwnid  29012  axpaschlem  29013  axpasch  29014  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  pthistrl  29796  clwwlkbp  30060  sticl  32290  hstcl  32292  slmdcmn  33287  rrextnrg  34158  rrextdrg  34159  rossspw  34326  srossspw  34333  eulerpartlemd  34523  eulerpartlemf  34527  eulerpartlemgvv  34533  eulerpartlemgu  34534  eulerpartlemgh  34535  eulerpartlemgs2  34537  eulerpartlemn  34538  bnj564  34900  bnj1366  34985  bnj545  35051  bnj548  35053  bnj558  35058  bnj570  35061  bnj580  35069  bnj929  35092  bnj998  35113  bnj1006  35116  bnj1190  35164  bnj1523  35227  msrval  35732  mthmpps  35776  eqvrelrefrel  38851  atllat  39556  stoweidlem60  46300  fourierdlem111  46457  modmknepk  47604  prproropf1o  47749  gpgedgvtx1  48304  arweutermc  49771