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 12800 ssnn0fi 13356 tmdcn2 22699 axcont 26764 numclwwlk3 28166 minvecolem3 28655 bnj556 32174 bnj557 32175 bnj1145 32267 btwnconn1lem4 33553 btwnconn1lem5 33554 btwnconn1lem6 33555 bj-ceqsalt 34204 bj-ceqsaltv 34205 |
Copyright terms: Public domain | W3C validator |