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  6393  smores2  8323  smofvon2  8325  smofvon  8328  errel  8680  elunitrn  13428  lincmb01cmp  13456  iccf1o  13457  elfznn0  13581  elfzouz  13624  ef01bndlem  16152  sin01bnd  16153  cos01bnd  16154  sin01gt0  16158  cos01gt0  16159  sin02gt0  16160  gzcn  16903  mresspw  17553  drsprs  18264  ipodrscl  18497  subgrcl  19063  pmtrfconj  19396  pgpprm  19523  slwprm  19539  efgsdmi  19662  efgsrel  19664  efgs1b  19666  efgsp1  19667  efgsres  19668  efgsfo  19669  efgredlema  19670  efgredlemf  19671  efgredlemd  19674  efgredlemc  19675  efgredlem  19677  efgrelexlemb  19680  efgcpbllemb  19685  rngabl  20064  srgcmn  20098  ringgrp  20147  irredcl  20333  subrngrcl  20460  sdrgrcl  20698  lmodgrp  20773  lssss  20842  phllvec  21538  obsrcl  21632  locfintop  23408  fclstop  23898  tmdmnd  23962  tgpgrp  23965  trgtgp  24055  tdrgtrg  24060  ust0  24107  ngpgrp  24487  elii1  24831  elii2  24832  icopnfcnv  24840  icopnfhmeo  24841  iccpnfhmeo  24843  xrhmeo  24844  oprpiece1res2  24850  phtpcer  24894  pcoval2  24916  pcoass  24924  clmlmod  24967  cphphl  25071  cphnlm  25072  cphsca  25079  bnnvc  25240  uc1pcl  26049  mon1pcl  26050  sinq12ge0  26417  cosq14ge0  26420  cosq34lt1  26436  cosord  26440  cos11  26442  recosf1o  26444  resinf1o  26445  efifo  26456  logrncn  26471  atanf  26790  atanneg  26817  efiatan  26822  atanlogaddlem  26823  atanlogadd  26824  atanlogsub  26826  efiatan2  26827  2efiatan  26828  tanatan  26829  areass  26869  dchrvmasumlem2  27409  dchrvmasumiflem1  27412  brbtwn2  28832  ax5seglem1  28855  ax5seglem2  28856  ax5seglem3  28858  ax5seglem5  28860  ax5seglem6  28861  ax5seglem9  28864  ax5seg  28865  axbtwnid  28866  axpaschlem  28867  axpasch  28868  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  pthistrl  29653  clwwlkbp  29914  sticl  32144  hstcl  32146  omndmnd  33018  slmdcmn  33158  orngring  33278  rrextnrg  33991  rrextdrg  33992  rossspw  34159  srossspw  34166  eulerpartlemd  34357  eulerpartlemf  34361  eulerpartlemgvv  34367  eulerpartlemgu  34368  eulerpartlemgh  34369  eulerpartlemgs2  34371  eulerpartlemn  34372  bnj564  34734  bnj1366  34819  bnj545  34885  bnj548  34887  bnj558  34892  bnj570  34895  bnj580  34903  bnj929  34926  bnj998  34947  bnj1006  34950  bnj1190  34998  bnj1523  35061  msrval  35525  mthmpps  35569  eqvrelrefrel  38589  atllat  39293  stoweidlem60  46058  fourierdlem111  46215  modmknepk  47363  prproropf1o  47508  gpgedgvtx1  48053  arweutermc  49519