Theorem simp1bi 1125

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  limord  6086  smores2  7792  smofvon2  7794  smofvon  7797  errel  8094  lincmb01cmp  12694  iccf1o  12695  elfznn0  12813  elfzouz  12855  ef01bndlem  15391  sin01bnd  15392  cos01bnd  15393  sin01gt0  15397  cos01gt0  15398  sin02gt0  15399  gzcn  16118  mresspw  16715  drsprs  17398  ipodrscl  17624  subgrcl  18062  pmtrfconj  18349  pgpprm  18473  slwprm  18489  efgsdmi  18610  efgsrel  18612  efgs1b  18614  efgsp1  18615  efgsres  18616  efgsresOLD  18617  efgsfo  18618  efgredlema  18619  efgredlemf  18620  efgredlemd  18623  efgredlemc  18624  efgredlem  18626  efgredlemOLD  18627  efgrelexlemb  18630  efgcpbllemb  18635  srgcmn  18975  ringgrp  19019  irredcl  19171  lmodgrp  19357  lssss  19424  phllvec  20469  obsrcl  20563  locfintop  21827  fclstop  22317  tmdmnd  22381  tgpgrp  22384  trgtgp  22473  tdrgtrg  22478  ust0  22525  ngpgrp  22905  elii1  23236  elii2  23237  icopnfcnv  23243  icopnfhmeo  23244  iccpnfhmeo  23246  xrhmeo  23247  oprpiece1res2  23253  phtpcer  23296  pcoval2  23317  pcoass  23325  clmlmod  23368  cphphl  23472  cphnlm  23473  cphsca  23480  bnnvc  23640  uc1pcl  24434  mon1pcl  24435  sinq12ge0  24791  cosq14ge0  24794  cosord  24811  cos11  24812  recosf1o  24814  resinf1o  24815  efifo  24826  logrncn  24841  atanf  25153  atanneg  25180  efiatan  25185  atanlogaddlem  25186  atanlogadd  25187  atanlogsub  25189  efiatan2  25190  2efiatan  25191  tanatan  25192  areass  25233  dchrvmasumlem2  25770  dchrvmasumiflem1  25773  brbtwn2  26388  ax5seglem1  26411  ax5seglem2  26412  ax5seglem3  26414  ax5seglem5  26416  ax5seglem6  26417  ax5seglem9  26420  ax5seg  26421  axbtwnid  26422  axpaschlem  26423  axpasch  26424  axcontlem2  26448  axcontlem4  26450  axcontlem7  26453  pthistrl  27208  clwwlkbp  27485  sticl  29767  hstcl  29769  omndmnd  30414  slmdcmn  30490  orngring  30543  elunitrn  30775  rrextnrg  30877  rrextdrg  30878  rossspw  31064  srossspw  31071  eulerpartlemd  31260  eulerpartlemf  31264  eulerpartlemgvv  31270  eulerpartlemgu  31271  eulerpartlemgh  31272  eulerpartlemgs2  31274  eulerpartlemn  31275  bnj564  31654  bnj1366  31740  bnj545  31805  bnj548  31807  bnj558  31812  bnj570  31815  bnj580  31823  bnj929  31846  bnj998  31866  bnj1006  31869  bnj1190  31916  bnj1523  31979  msrval  32275  mthmpps  32319  eqvrelrefrel  35256  atllat  35859  stoweidlem60  41755  fourierdlem111  41912  prproropf1o  43011  rngabl  43486