| 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 1152 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: syl3an1 1164 syl3anl1 1414 syl3anr1 1418 fnsuppres 8216 dif1en 9200 elfiun 9470 elioc2 13450 elico2 13451 elicc2 13452 dvdsleabs2 16349 subrngringnsg 20553 cphipval 25277 spthonpthon 29771 uhgrwkspth 29775 usgr2wlkspth 29779 upgriseupth 30226 cm2j 31639 bnj544 34908 btwnconn1lem4 36091 relowlssretop 37364 dalem53 39727 dalem54 39728 paddasslem14 39835 mzpcong 42984 itscnhlc0xyqsol 48686 |
| Copyright terms: Public domain | W3C validator |