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

Theorem 3anim3i 1155
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 1152 1 ((𝜒𝜃𝜑) → (𝜒𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  syl3an3  1166  syl3anl3  1415  syl3anr3  1419  elioo4g  13333  ssnn0fi  13899  tmdcn2  23463  axcont  27974  numclwwlk3  29378  minvecolem3  29867  bnj556  33576  bnj557  33577  bnj1145  33669  btwnconn1lem4  34728  btwnconn1lem5  34729  btwnconn1lem6  34730  bj-ceqsalt  35406  bj-ceqsaltv  35407
  Copyright terms: Public domain W3C validator