MPE Home 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