Theorem simp2bi 1012

Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
3simp1bi.1

Assertion

Ref	Expression
simp2bi

Proof of Theorem simp2bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3
2	1	biimpi 194	. 2
3	2	simp2d 1009	1

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

This theorem is referenced by:  smodm  7041  erdm  7340  ixpfn  7495  winafp  9096  inar1  9174  inatsk  9177  tskuni  9182  grur1  9219  supmullem1  10534  supmullem2  10535  supmul  10536  eluzelz  11119  elfz3nn0  11801  cshco  12802  swrds2  12883  ef01bndlem  13919  sin01bnd  13920  cos01bnd  13921  sin01gt0  13925  bitsss  14076  smueqlem  14140  gznegcl  14453  gzcjcl  14454  gzaddcl  14455  gzmulcl  14456  gzabssqcl  14459  4sqlem4a  14469  cshwshashlem2  14581  structcnvcnv  14643  structfun  14644  xpsff1o  14965  mre1cl  14991  drsbn0  15566  subgss  16202  symgfixelsi  16460  psgnunilem5  16519  pgpgrp  16614  slwsubg  16630  efgs1b  16754  efgsp1  16755  efgsres  16756  efgredeu  16770  efgred2  16771  efgcpbllemb  16773  srgmgp  17162  ringmgp  17204  irrednu  17354  lmodring  17520  lmodprop2d  17572  lssn0  17587  phlsrng  18666  ocvss  18701  obsss  18755  locfinbas  20023  fclsfil  20511  tmdtps  20575  tgptmd  20578  trgring  20673  tdrgdrng  20676  ngpms  21120  icopnfcnv  21442  xrhmeo  21446  oprpiece1res2  21452  phtpcer  21495  pcoval2  21516  pcoass  21524  clmsca  21565  cphsqrtcl  21631  bncms  21783  itg2ge0  22142  uc1pn0  22546  mon1pn0  22547  sinq12ge0  22901  cosq14gt0  22903  cosq14ge0  22904  sinord  22921  recosf1o  22922  resinf1o  22923  logrnaddcl  22962  atanf  23211  atanneg  23238  atancj  23241  efiatan  23243  atanlogaddlem  23244  atanlogadd  23245  atanlogsub  23247  efiatan2  23248  2efiatan  23249  tanatan  23250  dvatan  23266  areambl  23288  rlimcnp  23295  emgt0  23336  harmoniclbnd  23338  harmonicbnd4  23340  2sqlem2  23639  2sqlem3  23641  dchrvmasumlem2  23683  dchrvmasumiflem1  23686  logdivbnd  23741  pntpbnd2  23772  pnt  23799  brbtwn2  24208  ax5seglem3  24234  ax5seglem6  24237  axpaschlem  24243  axcontlem2  24268  axcontlem4  24270  eengbas  24284  ebtwntg  24285  ecgrtg  24286  elntg  24287  clwwisshclwwlem  24806  subgores  25306  subgoid  25309  subgoinv  25310  subgoablo  25313  ghsubgolemOLD  25372  hst1a  27137  stge0  27143  sthil  27153  fsumrp0cl  27685  omndtos  27695  slmdsrg  27750  orngogrp  27791  elunitge0  27881  xrge0iifcnv  27915  xrge0iifcv  27916  xrge0iifiso  27917  rrextnlm  27984  rrextchr  27985  logbcl  28013  voliune  28201  volfiniune  28202  lgamgulmlem2  28572  msrval  28898  mclsppslem  28943  dfon2lem1  29215  dfrdg2  29228  cntotbnd  30292  heiborlem5  30311  heiborlem6  30312  stoweidlem60  31842  fourierdlem40  31929  fourierdlem78  31967  rngmgp  32684  bnj563  33800  bnj1212  33858  bnj1219  33859  bnj1366  33888  bnj1379  33889  bnj545  33953  bnj594  33970  bnj1118  34040  bnj1177  34062  bnj1190  34064  bnj1398  34090  bnj1417  34097  bnj1450  34106  bnj1312  34114  bnj1523  34127  bj-flbi3  34608  atl0dm  35027  dalem-ccly  35409

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