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 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  syl3an3  1166  syl3anl3  1416  syl3anr3  1420  elioo4g  13447  ssnn0fi  14026  tmdcn2  24097  axcont  28991  numclwwlk3  30404  minvecolem3  30895  bnj556  34914  bnj557  34915  bnj1145  35007  btwnconn1lem4  36091  btwnconn1lem5  36092  btwnconn1lem6  36093  bj-ceqsalt  36887  bj-ceqsaltv  36888  uhgrimisgrgric  47899
  Copyright terms: Public domain W3C validator