Theorem simp3bi 1013

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

Hypothesis

Ref	Expression
3simp1bi.1

Assertion

Ref	Expression
simp3bi

Proof of Theorem simp3bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3
2	1	biimpi 194	. 2
3	2	simp3d 1010	1

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

This theorem is referenced by:  limuni  4943  smores2  7044  ersym  7342  ertr  7345  fvixp  7494  undifixp  7525  fiint  7817  winalim2  9095  inar1  9174  supmullem1  10534  supmullem2  10535  supmul  10536  eluzle  11122  ef01bndlem  13919  sin01bnd  13920  cos01bnd  13921  sin01gt0  13925  divalglem6  14056  gznegcl  14453  gzcjcl  14454  gzaddcl  14455  gzmulcl  14456  gzabssqcl  14459  4sqlem4a  14469  prdsbasprj  14869  xpsff1o  14965  mreintcl  14992  drsdir  15564  subggrp  16204  pmtrfconj  16491  symggen  16495  psgnunilem1  16518  subgpgp  16617  slwispgp  16631  sylow2alem1  16637  oppglsm  16662  efgsdmi  16750  efgsrel  16752  efgsp1  16755  efgsres  16756  efgcpbllemb  16773  efgcpbl  16774  srgi  17163  srgrz  17177  srglz  17178  ringi  17211  ringsrg  17237  irredmul  17358  lmodlema  17517  lsscl  17589  phllmhm  18667  ipcj  18669  ipeq0  18673  ocvi  18700  obsip  18752  obsocv  18757  2ndcctbss  19956  locfinnei  20024  fclssscls  20519  tmdcn  20582  tgpinv  20584  trgtmd  20667  tdrgunit  20669  ngpds  21123  elii1  21435  elii2  21436  icopnfcnv  21442  icopnfhmeo  21443  iccpnfhmeo  21445  xrhmeo  21446  phtpcer  21495  pcoass  21524  clmsubrg  21566  cphnmfval  21639  bnsca  21778  uc1pldg  22549  mon1pldg  22550  sinq12ge0  22901  cosq14gt0  22903  cosq14ge0  22904  sinord  22921  recosf1o  22922  resinf1o  22923  logrnaddcl  22962  logimul  22999  dvlog2lem  23033  atanf  23211  atanneg  23238  atancj  23241  efiatan  23243  atanlogaddlem  23244  atanlogadd  23245  atanlogsub  23247  efiatan2  23248  2efiatan  23249  ressatans  23265  dvatan  23266  areaf  23291  harmonicubnd  23339  harmonicbnd4  23340  2sqlem2  23639  2sqlem3  23641  dchrvmasumiflem1  23686  pntpbnd2  23772  f1otrg  24174  f1otrge  24175  brbtwn2  24208  ax5seglem3  24234  axpaschlem  24243  axcontlem7  24273  subgores  25306  hstel2  27138  stle1  27144  stj  27154  xrge0adddir  27682  omndadd  27696  slmdlema  27746  lmodslmd  27747  orngmul  27793  xrge0iifcnv  27915  xrge0iifiso  27917  xrge0iifhom  27919  rrextcusp  27986  rrextust  27989  sibfinima  28281  eulerpartlemf  28309  eulerpartlemgvv  28315  lgamgulmlem2  28572  snmlflim  28777  msrval  28898  mclsssvlem  28922  mclsind  28930  cntotbnd  30292  heiborlem8  30314  dmnnzd  30472  kelac1  31009  binomcxplemcvg  31259  binomcxplemnotnn0  31261  stoweidlem39  31821  stoweidlem60  31842  fourierdlem40  31929  fourierdlem78  31967  isringrng  32687  bnj563  33800  bnj1366  33888  bnj1379  33889  bnj554  33957  bnj557  33959  bnj570  33963  bnj594  33970  bnj1001  34016  bnj1006  34017  bnj1097  34037  bnj1177  34062  bnj1388  34089  bnj1398  34090  bnj1450  34106  bnj1501  34123  bnj1523  34127  bj-flbi3  34608  atlex  35041

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