Theorem simp1bi 1143

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 1140	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  limord  6310  smores2  8156  smofvon2  8158  smofvon  8161  errel  8465  elunitrn  13128  lincmb01cmp  13156  iccf1o  13157  elfznn0  13278  elfzouz  13320  ef01bndlem  15821  sin01bnd  15822  cos01bnd  15823  sin01gt0  15827  cos01gt0  15828  sin02gt0  15829  gzcn  16561  mresspw  17218  drsprs  17936  ipodrscl  18171  subgrcl  18675  pmtrfconj  18989  pgpprm  19113  slwprm  19129  efgsdmi  19253  efgsrel  19255  efgs1b  19257  efgsp1  19258  efgsres  19259  efgsfo  19260  efgredlema  19261  efgredlemf  19262  efgredlemd  19265  efgredlemc  19266  efgredlem  19268  efgrelexlemb  19271  efgcpbllemb  19276  srgcmn  19659  ringgrp  19703  irredcl  19861  lmodgrp  20045  lssss  20113  phllvec  20746  obsrcl  20840  locfintop  22580  fclstop  23070  tmdmnd  23134  tgpgrp  23137  trgtgp  23227  tdrgtrg  23232  ust0  23279  ngpgrp  23661  elii1  24004  elii2  24005  icopnfcnv  24011  icopnfhmeo  24012  iccpnfhmeo  24014  xrhmeo  24015  oprpiece1res2  24021  phtpcer  24064  pcoval2  24085  pcoass  24093  clmlmod  24136  cphphl  24240  cphnlm  24241  cphsca  24248  bnnvc  24409  uc1pcl  25213  mon1pcl  25214  sinq12ge0  25570  cosq14ge0  25573  cosq34lt1  25588  cosord  25592  cos11  25594  recosf1o  25596  resinf1o  25597  efifo  25608  logrncn  25623  atanf  25935  atanneg  25962  efiatan  25967  atanlogaddlem  25968  atanlogadd  25969  atanlogsub  25971  efiatan2  25972  2efiatan  25973  tanatan  25974  areass  26014  dchrvmasumlem2  26551  dchrvmasumiflem1  26554  brbtwn2  27176  ax5seglem1  27199  ax5seglem2  27200  ax5seglem3  27202  ax5seglem5  27204  ax5seglem6  27205  ax5seglem9  27208  ax5seg  27209  axbtwnid  27210  axpaschlem  27211  axpasch  27212  axcontlem2  27236  axcontlem4  27238  axcontlem7  27241  pthistrl  27994  clwwlkbp  28250  sticl  30478  hstcl  30480  omndmnd  31232  slmdcmn  31360  orngring  31401  rrextnrg  31851  rrextdrg  31852  rossspw  32037  srossspw  32044  eulerpartlemd  32233  eulerpartlemf  32237  eulerpartlemgvv  32243  eulerpartlemgu  32244  eulerpartlemgh  32245  eulerpartlemgs2  32247  eulerpartlemn  32248  bnj564  32624  bnj1366  32709  bnj545  32775  bnj548  32777  bnj558  32782  bnj570  32785  bnj580  32793  bnj929  32816  bnj998  32837  bnj1006  32840  bnj1190  32888  bnj1523  32951  msrval  33400  mthmpps  33444  eqvrelrefrel  36638  atllat  37241  stoweidlem60  43491  fourierdlem111  43648  prproropf1o  44847  rngabl  45323