![]() |
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 13384 ssnn0fi 13950 tmdcn2 23593 axcont 28234 numclwwlk3 29638 minvecolem3 30129 bnj556 33911 bnj557 33912 bnj1145 34004 btwnconn1lem4 35062 btwnconn1lem5 35063 btwnconn1lem6 35064 bj-ceqsalt 35766 bj-ceqsaltv 35767 |
Copyright terms: Public domain | W3C validator |