![]() |
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 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 13381 ssnn0fi 13947 tmdcn2 23585 axcont 28224 numclwwlk3 29628 minvecolem3 30117 bnj556 33900 bnj557 33901 bnj1145 33993 btwnconn1lem4 35051 btwnconn1lem5 35052 btwnconn1lem6 35053 bj-ceqsalt 35755 bj-ceqsaltv 35756 |
Copyright terms: Public domain | W3C validator |