Theorem simp1bi 1076

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  limord  5784  smores2  7451  smofvon2  7453  smofvon  7456  errel  7751  lincmb01cmp  12315  iccf1o  12316  elfznn0  12433  elfzouz  12474  ef01bndlem  14914  sin01bnd  14915  cos01bnd  14916  sin01gt0  14920  cos01gt0  14921  sin02gt0  14922  gzcn  15636  mresspw  16252  drsprs  16936  ipodrscl  17162  subgrcl  17599  pmtrfconj  17886  pgpprm  18008  slwprm  18024  efgsdmi  18145  efgsrel  18147  efgs1b  18149  efgsp1  18150  efgsres  18151  efgsfo  18152  efgredlema  18153  efgredlemf  18154  efgredlemd  18157  efgredlemc  18158  efgredlem  18160  efgrelexlemb  18163  efgcpbllemb  18168  srgcmn  18508  ringgrp  18552  irredcl  18704  lmodgrp  18870  lssss  18937  phllvec  19974  obsrcl  20067  locfintop  21324  fclstop  21815  tmdmnd  21879  tgpgrp  21882  trgtgp  21971  tdrgtrg  21976  ust0  22023  ngpgrp  22403  elii1  22734  elii2  22735  icopnfcnv  22741  icopnfhmeo  22742  iccpnfhmeo  22744  xrhmeo  22745  oprpiece1res1  22750  oprpiece1res2  22751  phtpcer  22794  phtpcerOLD  22795  pcoval2  22816  pcoass  22824  clmlmod  22867  cphphl  22971  cphnlm  22972  cphsca  22979  bnnvc  23137  uc1pcl  23903  mon1pcl  23904  sinq12ge0  24260  cosq14ge0  24263  cosord  24278  cos11  24279  recosf1o  24281  resinf1o  24282  efifo  24293  logrncn  24309  atanf  24607  atanneg  24634  efiatan  24639  atanlogaddlem  24640  atanlogadd  24641  atanlogsub  24643  efiatan2  24644  2efiatan  24645  tanatan  24646  areass  24686  dchrvmasumlem2  25187  dchrvmasumiflem1  25190  brbtwn2  25785  ax5seglem1  25808  ax5seglem2  25809  ax5seglem3  25811  ax5seglem5  25813  ax5seglem6  25814  ax5seglem9  25817  ax5seg  25818  axbtwnid  25819  axpaschlem  25820  axpasch  25821  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  pthistrl  26621  clwwlkbp  26883  sticl  29074  hstcl  29076  omndmnd  29704  slmdcmn  29758  orngring  29800  elunitrn  29943  rrextnrg  30045  rrextdrg  30046  rossspw  30232  srossspw  30239  eulerpartlemd  30428  eulerpartlemf  30432  eulerpartlemgvv  30438  eulerpartlemgu  30439  eulerpartlemgh  30440  eulerpartlemgs2  30442  eulerpartlemn  30443  bnj564  30814  bnj1366  30900  bnj545  30965  bnj548  30967  bnj558  30972  bnj570  30975  bnj580  30983  bnj929  31006  bnj998  31026  bnj1006  31029  bnj1190  31076  bnj1523  31139  msrval  31435  mthmpps  31479  atllat  34587  stoweidlem60  40277  fourierdlem111  40434  rngabl  41877