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

Theorem 3anim3i 1248
 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 1245 1 ((𝜒𝜃𝜑) → (𝜒𝜃𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1036 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 386  df-3an 1038 This theorem is referenced by:  syl3anl3  1374  syl3anr3  1378  elioo4g  12219  ssnn0fi  12767  tmdcn2  21874  axcont  25837  1ewlk  26956  1pthon2ve  26994  numclwwlk3  27213  minvecolem3  27702  bnj556  30944  bnj557  30945  bnj1145  31035  btwnconn1lem4  32172  btwnconn1lem5  32173  btwnconn1lem6  32174  bj-ceqsalt  32850  bj-ceqsaltv  32851
 Copyright terms: Public domain W3C validator