Theorem simp1bi 1011

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 194	. 2
3	2	simp1d 1008	1

Syntax hints:  ->wi 4  <->wb 184  /\w3a 973

This theorem is referenced by:  limord  4942  smores2  7044  smofvon2  7046  smofvon  7049  errel  7339  lincmb01cmp  11692  iccf1o  11693  elfznn0  11800  elfzouz  11833  ef01bndlem  13919  sin01bnd  13920  cos01bnd  13921  sin01gt0  13925  cos01gt0  13926  sin02gt0  13927  gzcn  14450  mresspw  14989  drsprs  15565  ipodrscl  15792  subgrcl  16206  pmtrfconj  16491  pgpprm  16613  slwprm  16629  efgsdmi  16750  efgsrel  16752  efgs1b  16754  efgsp1  16755  efgsres  16756  efgsfo  16757  efgredlema  16758  efgredlemf  16759  efgredlemd  16762  efgredlemc  16763  efgredlem  16765  efgrelexlemb  16768  efgcpbllemb  16773  srgcmn  17160  ringgrp  17203  irredcl  17353  lmodgrp  17519  lssss  17583  phllvec  18664  obsrcl  18754  locfintop  20022  fclstop  20512  tmdmnd  20574  tgpgrp  20577  trgtgp  20670  tdrgtrg  20675  ust0  20722  ngpgrp  21119  elii1  21435  elii2  21436  icopnfcnv  21442  icopnfhmeo  21443  iccpnfhmeo  21445  xrhmeo  21446  oprpiece1res1  21451  oprpiece1res2  21452  phtpcer  21495  pcoval2  21516  pcoass  21524  clmlmod  21567  cphphl  21618  cphnlm  21619  cphsca  21626  bnnvc  21779  uc1pcl  22544  mon1pcl  22545  sinq12ge0  22901  cosq14ge0  22904  cosord  22919  cos11  22920  recosf1o  22922  resinf1o  22923  efifo  22934  logrncn  22950  atanf  23211  atanneg  23238  efiatan  23243  atanlogaddlem  23244  atanlogadd  23245  atanlogsub  23247  efiatan2  23248  2efiatan  23249  tanatan  23250  areass  23289  dchrvmasumlem2  23683  dchrvmasumiflem1  23686  brbtwn2  24208  ax5seglem1  24231  ax5seglem2  24232  ax5seglem3  24234  ax5seglem5  24236  ax5seglem6  24237  ax5seglem9  24240  ax5seg  24241  axbtwnid  24242  axpaschlem  24243  axpasch  24244  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  2spotiundisj  25062  subgores  25306  subgoid  25309  subgoinv  25310  sticl  27134  hstcl  27136  omndmnd  27694  slmdcmn  27748  orngring  27790  elunitrn  27879  rrextnrg  27982  rrextdrg  27983  eulerpartlemd  28305  eulerpartlemf  28309  eulerpartlemgvv  28315  eulerpartlemgu  28316  eulerpartlemgh  28317  eulerpartlemgs2  28319  eulerpartlemn  28320  msrval  28898  mthmpps  28942  stoweidlem60  31842  fourierdlem111  32000  rngabl  32683  bnj564  33801  bnj1366  33888  bnj545  33953  bnj548  33955  bnj558  33960  bnj570  33963  bnj580  33971  bnj929  33994  bnj998  34014  bnj1006  34017  bnj1190  34064  bnj1523  34127  atllat  35025

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 185  df-an 371  df-3an 975