| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sylanr2 | Structured version Visualization version GIF version | ||
| Description: A syllogism inference. (Contributed by NM, 9-Apr-2005.) |
| Ref | Expression |
|---|---|
| sylanr2.1 | ⊢ (𝜑 → 𝜃) |
| sylanr2.2 | ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏) |
| Ref | Expression |
|---|---|
| sylanr2 | ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜑)) → 𝜏) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sylanr2.1 | . . 3 ⊢ (𝜑 → 𝜃) | |
| 2 | 1 | anim2i 617 | . 2 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜃)) |
| 3 | sylanr2.2 | . 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
| 4 | 2, 3 | sylan2 593 | 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: adantrrl 724 adantrrr 725 unfi 9211 isfin7-2 10436 mulsub 11706 fzsubel 13600 expsub 14151 ramlb 17057 0ram 17058 ressmplvsca 22049 tgcl 22976 fgss2 23882 nmoid 24763 madebdaylemlrcut 27937 numclwwlkqhash 30394 chirredlem4 32412 pibt2 37418 lindsadd 37620 poimirlem28 37655 pridlc3 38080 stoweidlem34 46049 |
| Copyright terms: Public domain | W3C validator |