MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anim3i Unicode version

Theorem 3anim3i 1184
Description: Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.)
Hypothesis
Ref Expression
3animi.1
Assertion
Ref Expression
3anim3i

Proof of Theorem 3anim3i
StepHypRef Expression
1 id 22 . 2
2 id 22 . 2
3 3animi.1 . 2
41, 2, 33anim123i 1181 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  syl3anl3  1278  syl3anr3  1282  elioo4g  11614  ssnn0fi  12094  tmdcn2  20588  axcont  24279  constr3lem4  24647  extwwlkfab  25090  minvecolem3  25792  btwnconn1lem4  29740  btwnconn1lem5  29741  btwnconn1lem6  29742  bnj556  33958  bnj557  33959  bnj1145  34049  bj-ceqsalt  34451  bj-ceqsaltv  34452
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
  Copyright terms: Public domain W3C validator