Theorem simp1bi 1144

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 1141	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  6445  smores2  8392  smofvon2  8394  smofvon  8397  errel  8752  elunitrn  13503  lincmb01cmp  13531  iccf1o  13532  elfznn0  13656  elfzouz  13699  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  sin01gt0  16222  cos01gt0  16223  sin02gt0  16224  gzcn  16965  mresspw  17636  drsprs  18360  ipodrscl  18595  subgrcl  19161  pmtrfconj  19498  pgpprm  19625  slwprm  19641  efgsdmi  19764  efgsrel  19766  efgs1b  19768  efgsp1  19769  efgsres  19770  efgsfo  19771  efgredlema  19772  efgredlemf  19773  efgredlemd  19776  efgredlemc  19777  efgredlem  19779  efgrelexlemb  19782  efgcpbllemb  19787  rngabl  20172  srgcmn  20206  ringgrp  20255  irredcl  20440  subrngrcl  20567  sdrgrcl  20806  lmodgrp  20881  lssss  20951  phllvec  21664  obsrcl  21760  locfintop  23544  fclstop  24034  tmdmnd  24098  tgpgrp  24101  trgtgp  24191  tdrgtrg  24196  ust0  24243  ngpgrp  24627  elii1  24977  elii2  24978  icopnfcnv  24986  icopnfhmeo  24987  iccpnfhmeo  24989  xrhmeo  24990  oprpiece1res2  24996  phtpcer  25040  pcoval2  25062  pcoass  25070  clmlmod  25113  cphphl  25218  cphnlm  25219  cphsca  25226  bnnvc  25387  uc1pcl  26197  mon1pcl  26198  sinq12ge0  26564  cosq14ge0  26567  cosq34lt1  26583  cosord  26587  cos11  26589  recosf1o  26591  resinf1o  26592  efifo  26603  logrncn  26618  atanf  26937  atanneg  26964  efiatan  26969  atanlogaddlem  26970  atanlogadd  26971  atanlogsub  26973  efiatan2  26974  2efiatan  26975  tanatan  26976  areass  27016  dchrvmasumlem2  27556  dchrvmasumiflem1  27559  brbtwn2  28934  ax5seglem1  28957  ax5seglem2  28958  ax5seglem3  28960  ax5seglem5  28962  ax5seglem6  28963  ax5seglem9  28966  ax5seg  28967  axbtwnid  28968  axpaschlem  28969  axpasch  28970  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  pthistrl  29757  clwwlkbp  30013  sticl  32243  hstcl  32245  omndmnd  33063  slmdcmn  33193  orngring  33309  rrextnrg  33963  rrextdrg  33964  rossspw  34149  srossspw  34156  eulerpartlemd  34347  eulerpartlemf  34351  eulerpartlemgvv  34357  eulerpartlemgu  34358  eulerpartlemgh  34359  eulerpartlemgs2  34361  eulerpartlemn  34362  bnj564  34736  bnj1366  34821  bnj545  34887  bnj548  34889  bnj558  34894  bnj570  34897  bnj580  34905  bnj929  34928  bnj998  34949  bnj1006  34952  bnj1190  35000  bnj1523  35063  msrval  35522  mthmpps  35566  eqvrelrefrel  38579  atllat  39281  stoweidlem60  46015  fourierdlem111  46172  prproropf1o  47431  gpgedgvtx1  47954  gpg3nbgrvtxlem  47957