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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  limord  6329  smores2  8194  smofvon2  8196  smofvon  8199  errel  8516  elunitrn  13208  lincmb01cmp  13236  iccf1o  13237  elfznn0  13358  elfzouz  13400  ef01bndlem  15902  sin01bnd  15903  cos01bnd  15904  sin01gt0  15908  cos01gt0  15909  sin02gt0  15910  gzcn  16642  mresspw  17310  drsprs  18030  ipodrscl  18265  subgrcl  18769  pmtrfconj  19083  pgpprm  19207  slwprm  19223  efgsdmi  19347  efgsrel  19349  efgs1b  19351  efgsp1  19352  efgsres  19353  efgsfo  19354  efgredlema  19355  efgredlemf  19356  efgredlemd  19359  efgredlemc  19360  efgredlem  19362  efgrelexlemb  19365  efgcpbllemb  19370  srgcmn  19753  ringgrp  19797  irredcl  19955  lmodgrp  20139  lssss  20207  phllvec  20843  obsrcl  20939  locfintop  22681  fclstop  23171  tmdmnd  23235  tgpgrp  23238  trgtgp  23328  tdrgtrg  23333  ust0  23380  ngpgrp  23764  elii1  24107  elii2  24108  icopnfcnv  24114  icopnfhmeo  24115  iccpnfhmeo  24117  xrhmeo  24118  oprpiece1res2  24124  phtpcer  24167  pcoval2  24188  pcoass  24196  clmlmod  24239  cphphl  24344  cphnlm  24345  cphsca  24352  bnnvc  24513  uc1pcl  25317  mon1pcl  25318  sinq12ge0  25674  cosq14ge0  25677  cosq34lt1  25692  cosord  25696  cos11  25698  recosf1o  25700  resinf1o  25701  efifo  25712  logrncn  25727  atanf  26039  atanneg  26066  efiatan  26071  atanlogaddlem  26072  atanlogadd  26073  atanlogsub  26075  efiatan2  26076  2efiatan  26077  tanatan  26078  areass  26118  dchrvmasumlem2  26655  dchrvmasumiflem1  26658  brbtwn2  27282  ax5seglem1  27305  ax5seglem2  27306  ax5seglem3  27308  ax5seglem5  27310  ax5seglem6  27311  ax5seglem9  27314  ax5seg  27315  axbtwnid  27316  axpaschlem  27317  axpasch  27318  axcontlem2  27342  axcontlem4  27344  axcontlem7  27347  pthistrl  28102  clwwlkbp  28358  sticl  30586  hstcl  30588  omndmnd  31339  slmdcmn  31467  orngring  31508  rrextnrg  31960  rrextdrg  31961  rossspw  32146  srossspw  32153  eulerpartlemd  32342  eulerpartlemf  32346  eulerpartlemgvv  32352  eulerpartlemgu  32353  eulerpartlemgh  32354  eulerpartlemgs2  32356  eulerpartlemn  32357  bnj564  32733  bnj1366  32818  bnj545  32884  bnj548  32886  bnj558  32891  bnj570  32894  bnj580  32902  bnj929  32925  bnj998  32946  bnj1006  32949  bnj1190  32997  bnj1523  33060  msrval  33509  mthmpps  33553  eqvrelrefrel  36718  atllat  37321  stoweidlem60  43608  fourierdlem111  43765  prproropf1o  44970  rngabl  45446