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

Theorem 3anim3i 1242
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 1239 1 ((𝜒𝜃𝜑) → (𝜒𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  syl3anl3  1367  syl3anr3  1371  elioo4g  12056  ssnn0fi  12596  tmdcn2  21640  axcont  25569  constr3lem4  25936  extwwlkfab  26378  minvecolem3  26917  bnj556  30025  bnj557  30026  bnj1145  30116  btwnconn1lem4  31168  btwnconn1lem5  31169  btwnconn1lem6  31170  bj-ceqsalt  31867  bj-ceqsaltv  31868  1ewlk  41280  1pthon2ve  41318  av-numclwwlk3  41536
  Copyright terms: Public domain W3C validator