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

Theorem 3anim3i 1157
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 1154 1 ((𝜒𝜃𝜑) → (𝜒𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1071
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 197  df-an 383  df-3an 1073
This theorem is referenced by:  syl3an3  1169  syl3anl3  1523  syl3anr3  1528  elioo4g  12439  ssnn0fi  12992  tmdcn2  22113  axcont  26077  1ewlk  27295  1pthon2ve  27334  numclwwlk3  27584  minvecolem3  28072  bnj556  31308  bnj557  31309  bnj1145  31399  btwnconn1lem4  32534  btwnconn1lem5  32535  btwnconn1lem6  32536  bj-ceqsalt  33204  bj-ceqsaltv  33205
  Copyright terms: Public domain W3C validator