Theorem simp1bi 1163

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  limord  6429  smores2  8350  smofvon2  8352  smofvon  8355  errel  8713  elunitrn  13512  lincmb01cmp  13540  iccf1o  13541  elfznn0  13667  elfzouz  13711  ef01bndlem  16265  sin01bnd  16266  cos01bnd  16267  sin01gt0  16271  cos01gt0  16272  sin02gt0  16273  gzcn  17017  mresspw  17669  drsprs  18384  ipodrscl  18619  subgrcl  19228  pmtrfconj  19567  pgpprm  19694  slwprm  19710  efgsdmi  19833  efgsrel  19835  efgs1b  19837  efgsp1  19838  efgsres  19839  efgsfo  19840  efgredlema  19841  efgredlemf  19842  efgredlemd  19845  efgredlemc  19846  efgredlem  19848  efgrelexlemb  19851  efgcpbllemb  19856  omndmnd  20227  rngabl  20264  srgcmn  20302  ringgrp  20351  irredcl  20539  subrngrcl  20687  sdrgrcl  20929  orngring  21002  lmodgrp  21025  lssss  21094  phllvec  21816  obsrcl  21910  locfintop  23715  fclstop  24205  tmdmnd  24269  tgpgrp  24272  trgtgp  24362  tdrgtrg  24367  ust0  24414  ngpgrp  24793  elii1  25131  elii2  25132  icopnfcnv  25138  icopnfhmeo  25139  iccpnfhmeo  25141  xrhmeo  25142  oprpiece1res2  25148  phtpcer  25191  pcoval2  25212  pcoass  25220  clmlmod  25263  cphphl  25367  cphnlm  25368  cphsca  25375  bnnvc  25536  uc1pcl  26338  mon1pcl  26339  sinq12ge0  26710  cosq14ge0  26713  cosq34lt1  26729  cosord  26733  cos11  26735  recosf1o  26737  resinf1o  26738  efifo  26749  logrncn  26764  atanf  27082  atanneg  27109  efiatan  27114  atanlogaddlem  27115  atanlogadd  27116  atanlogsub  27118  efiatan2  27119  2efiatan  27120  tanatan  27121  areass  27161  dchrvmasumlem2  27699  dchrvmasumiflem1  27702  brbtwn2  29292  ax5seglem1  29315  ax5seglem2  29316  ax5seglem3  29318  ax5seglem5  29320  ax5seglem6  29321  ax5seglem9  29324  ax5seg  29325  axbtwnid  29326  axpaschlem  29327  axpasch  29328  axcontlem2  29352  axcontlem4  29354  axcontlem7  29357  pthistrl  30109  clwwlkbp  30373  sticl  32604  hstcl  32606  slmdcmn  33556  rrextnrg  34422  rrextdrg  34423  rossspw  34591  srossspw  34598  eulerpartlemd  34788  eulerpartlemf  34792  eulerpartlemgvv  34798  eulerpartlemgu  34799  eulerpartlemgh  34800  eulerpartlemgs2  34802  eulerpartlemn  34803  bnj564  35165  bnj1366  35249  bnj545  35315  bnj548  35317  bnj558  35322  bnj570  35325  bnj580  35333  bnj929  35356  bnj998  35377  bnj1006  35380  bnj1190  35428  bnj1523  35491  msrval  36051  mthmpps  36095  eqvrelrefrel  39372  atllat  40115  stoweidlem60  46815  fourierdlem111  46972  modmknepk  48146  muldvdsfacgt  48164  prproropf1o  48297  gpgedgvtx1  48868  arweutermc  50349