Theorem simp1bi 1161

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  limord  6411  smores2  8329  smofvon2  8331  smofvon  8334  errel  8692  elunitrn  13485  lincmb01cmp  13513  iccf1o  13514  elfznn0  13639  elfzouz  13683  ef01bndlem  16230  sin01bnd  16231  cos01bnd  16232  sin01gt0  16236  cos01gt0  16237  sin02gt0  16238  gzcn  16982  mresspw  17634  drsprs  18349  ipodrscl  18584  subgrcl  19188  pmtrfconj  19527  pgpprm  19654  slwprm  19670  efgsdmi  19793  efgsrel  19795  efgs1b  19797  efgsp1  19798  efgsres  19799  efgsfo  19800  efgredlema  19801  efgredlemf  19802  efgredlemd  19805  efgredlemc  19806  efgredlem  19808  efgrelexlemb  19811  efgcpbllemb  19816  omndmnd  20187  rngabl  20224  srgcmn  20262  ringgrp  20311  irredcl  20497  subrngrcl  20627  sdrgrcl  20861  orngring  20934  lmodgrp  20957  lssss  21026  phllvec  21739  obsrcl  21833  locfintop  23639  fclstop  24129  tmdmnd  24193  tgpgrp  24196  trgtgp  24286  tdrgtrg  24291  ust0  24338  ngpgrp  24717  elii1  25055  elii2  25056  icopnfcnv  25062  icopnfhmeo  25063  iccpnfhmeo  25065  xrhmeo  25066  oprpiece1res2  25072  phtpcer  25115  pcoval2  25136  pcoass  25144  clmlmod  25187  cphphl  25291  cphnlm  25292  cphsca  25299  bnnvc  25460  uc1pcl  26262  mon1pcl  26263  sinq12ge0  26631  cosq14ge0  26634  cosq34lt1  26650  cosord  26654  cos11  26656  recosf1o  26658  resinf1o  26659  efifo  26670  logrncn  26685  atanf  27003  atanneg  27030  efiatan  27035  atanlogaddlem  27036  atanlogadd  27037  atanlogsub  27039  efiatan2  27040  2efiatan  27041  tanatan  27042  areass  27082  dchrvmasumlem2  27620  dchrvmasumiflem1  27623  brbtwn2  29164  ax5seglem1  29187  ax5seglem2  29188  ax5seglem3  29190  ax5seglem5  29192  ax5seglem6  29193  ax5seglem9  29196  ax5seg  29197  axbtwnid  29198  axpaschlem  29199  axpasch  29200  axcontlem2  29224  axcontlem4  29226  axcontlem7  29229  pthistrl  29981  clwwlkbp  30245  sticl  32476  hstcl  32478  slmdcmn  33438  rrextnrg  34308  rrextdrg  34309  rossspw  34476  srossspw  34483  eulerpartlemd  34673  eulerpartlemf  34677  eulerpartlemgvv  34683  eulerpartlemgu  34684  eulerpartlemgh  34685  eulerpartlemgs2  34687  eulerpartlemn  34688  bnj564  35050  bnj1366  35134  bnj545  35200  bnj548  35202  bnj558  35207  bnj570  35210  bnj580  35218  bnj929  35241  bnj998  35262  bnj1006  35265  bnj1190  35313  bnj1523  35376  msrval  35901  mthmpps  35945  eqvrelrefrel  39193  atllat  39936  stoweidlem60  46632  fourierdlem111  46789  modmknepk  47960  muldvdsfacgt  47978  prproropf1o  48111  gpgedgvtx1  48682  arweutermc  50159