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

Theorem 3anim3i 1151
 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 1148 1 ((𝜒𝜃𝜑) → (𝜒𝜃𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  syl3an3  1162  syl3anl3  1411  syl3anr3  1415  elioo4g  12785  ssnn0fi  13348  tmdcn2  22694  axcont  26770  numclwwlk3  28170  minvecolem3  28659  bnj556  32282  bnj557  32283  bnj1145  32375  btwnconn1lem4  33664  btwnconn1lem5  33665  btwnconn1lem6  33666  bj-ceqsalt  34326  bj-ceqsaltv  34327
 Copyright terms: Public domain W3C validator