Theorem simp1bi 1146

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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

This theorem is referenced by:  limord  6384  smores2  8294  smofvon2  8296  smofvon  8299  errel  8653  elunitrn  13420  lincmb01cmp  13448  iccf1o  13449  elfznn0  13574  elfzouz  13618  ef01bndlem  16151  sin01bnd  16152  cos01bnd  16153  sin01gt0  16157  cos01gt0  16158  sin02gt0  16159  gzcn  16903  mresspw  17554  drsprs  18269  ipodrscl  18504  subgrcl  19107  pmtrfconj  19441  pgpprm  19568  slwprm  19584  efgsdmi  19707  efgsrel  19709  efgs1b  19711  efgsp1  19712  efgsres  19713  efgsfo  19714  efgredlema  19715  efgredlemf  19716  efgredlemd  19719  efgredlemc  19720  efgredlem  19722  efgrelexlemb  19725  efgcpbllemb  19730  omndmnd  20101  rngabl  20136  srgcmn  20170  ringgrp  20219  irredcl  20404  subrngrcl  20528  sdrgrcl  20766  orngring  20839  lmodgrp  20862  lssss  20931  phllvec  21609  obsrcl  21703  locfintop  23486  fclstop  23976  tmdmnd  24040  tgpgrp  24043  trgtgp  24133  tdrgtrg  24138  ust0  24185  ngpgrp  24564  elii1  24902  elii2  24903  icopnfcnv  24909  icopnfhmeo  24910  iccpnfhmeo  24912  xrhmeo  24913  oprpiece1res2  24919  phtpcer  24962  pcoval2  24983  pcoass  24991  clmlmod  25034  cphphl  25138  cphnlm  25139  cphsca  25146  bnnvc  25307  uc1pcl  26109  mon1pcl  26110  sinq12ge0  26472  cosq14ge0  26475  cosq34lt1  26491  cosord  26495  cos11  26497  recosf1o  26499  resinf1o  26500  efifo  26511  logrncn  26526  atanf  26844  atanneg  26871  efiatan  26876  atanlogaddlem  26877  atanlogadd  26878  atanlogsub  26880  efiatan2  26881  2efiatan  26882  tanatan  26883  areass  26923  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  brbtwn2  28974  ax5seglem1  28997  ax5seglem2  28998  ax5seglem3  29000  ax5seglem5  29002  ax5seglem6  29003  ax5seglem9  29006  ax5seg  29007  axbtwnid  29008  axpaschlem  29009  axpasch  29010  axcontlem2  29034  axcontlem4  29036  axcontlem7  29039  pthistrl  29791  clwwlkbp  30055  sticl  32286  hstcl  32288  slmdcmn  33266  rrextnrg  34145  rrextdrg  34146  rossspw  34313  srossspw  34320  eulerpartlemd  34510  eulerpartlemf  34514  eulerpartlemgvv  34520  eulerpartlemgu  34521  eulerpartlemgh  34522  eulerpartlemgs2  34524  eulerpartlemn  34525  bnj564  34887  bnj1366  34971  bnj545  35037  bnj548  35039  bnj558  35044  bnj570  35047  bnj580  35055  bnj929  35078  bnj998  35099  bnj1006  35102  bnj1190  35150  bnj1523  35213  msrval  35720  mthmpps  35764  eqvrelrefrel  39003  atllat  39746  stoweidlem60  46488  fourierdlem111  46645  modmknepk  47816  muldvdsfacgt  47834  prproropf1o  47967  gpgedgvtx1  48538  arweutermc  50005