Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3anim1i | Structured version Visualization version GIF version |
Description: Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.) |
Ref | Expression |
---|---|
3animi.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
3anim1i | ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3animi.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | id 22 | . 2 ⊢ (𝜒 → 𝜒) | |
3 | id 22 | . 2 ⊢ (𝜃 → 𝜃) | |
4 | 1, 2, 3 | 3anim123i 1247 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: syl3an1 1359 syl3anl1 1374 syl3anr1 1378 fnsuppres 7322 elfiun 8336 elioc2 12236 elico2 12237 elicc2 12238 dvdsleabs2 15034 mulgnndir 17569 mulgnnass 17576 cphipval 23042 spthonpthon 26647 uhgrwkspth 26651 usgr2wlkspth 26655 upgriseupth 27067 cm2j 28479 bnj544 30964 btwnconn1lem4 32197 relowlssretop 33211 dalem53 35011 dalem54 35012 paddasslem14 35119 mzpcong 37539 |
Copyright terms: Public domain | W3C validator |