| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > syl2ani | Structured version Visualization version GIF version | ||
| Description: A syllogism inference. (Contributed by NM, 3-Aug-1999.) |
| Ref | Expression |
|---|---|
| syl2ani.1 | ⊢ (𝜑 → 𝜒) |
| syl2ani.2 | ⊢ (𝜂 → 𝜃) |
| syl2ani.3 | ⊢ (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)) |
| Ref | Expression |
|---|---|
| syl2ani | ⊢ (𝜓 → ((𝜑 ∧ 𝜂) → 𝜏)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syl2ani.1 | . 2 ⊢ (𝜑 → 𝜒) | |
| 2 | syl2ani.2 | . . 3 ⊢ (𝜂 → 𝜃) | |
| 3 | syl2ani.3 | . . 3 ⊢ (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)) | |
| 4 | 2, 3 | sylan2i 606 | . 2 ⊢ (𝜓 → ((𝜒 ∧ 𝜂) → 𝜏)) |
| 5 | 1, 4 | sylani 604 | 1 ⊢ (𝜓 → ((𝜑 ∧ 𝜂) → 𝜏)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 |
| This theorem is referenced by: 2mo 2648 fvf1pr 7327 frxp 8151 poxp2 8168 mapen 9181 rex2dom 9282 fin1a2lem9 10448 coprmproddvdslem 16699 psss 18625 mgmidmo 18673 aannenlem1 26370 funtransport 36032 cgrxfr 36056 btwnxfr 36057 weiunpo 36466 bj-cbv3tb 36788 |
| Copyright terms: Public domain | W3C validator |