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 1143 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: syl3an1 1155 syl3anl1 1404 syl3anr1 1408 fnsuppres 7846 elfiun 8882 elioc2 12787 elico2 12788 elicc2 12789 dvdsleabs2 15650 cphipval 23773 spthonpthon 27459 uhgrwkspth 27463 usgr2wlkspth 27467 upgriseupth 27913 cm2j 29324 bnj544 32065 btwnconn1lem4 33448 relowlssretop 34526 dalem53 36741 dalem54 36742 paddasslem14 36849 mzpcong 39447 itscnhlc0xyqsol 44680 |
Copyright terms: Public domain | W3C validator |