Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3anim3i | Structured version Visualization version GIF version |
Description: Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.) |
Ref | Expression |
---|---|
3animi.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
3anim3i | ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝜒 → 𝜒) | |
2 | id 22 | . 2 ⊢ (𝜃 → 𝜃) | |
3 | 3animi.1 | . 2 ⊢ (𝜑 → 𝜓) | |
4 | 1, 2, 3 | 3anim123i 1147 | 1 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1083 |
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 209 df-an 399 df-3an 1085 |
This theorem is referenced by: syl3an3 1161 syl3anl3 1410 syl3anr3 1414 elioo4g 12798 ssnn0fi 13354 tmdcn2 22697 axcont 26762 numclwwlk3 28164 minvecolem3 28653 bnj556 32172 bnj557 32173 bnj1145 32265 btwnconn1lem4 33551 btwnconn1lem5 33552 btwnconn1lem6 33553 bj-ceqsalt 34205 bj-ceqsaltv 34206 |
Copyright terms: Public domain | W3C validator |