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 618 | . 2 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜃)) |
3 | sylanr2.2 | . 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
4 | 2, 3 | sylan2 594 | 1 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜑)) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: adantrrl 722 adantrrr 723 isfin7-2 9812 mulsub 11077 fzsubel 12937 expsub 13471 ramlb 16349 0ram 16350 ressmplvsca 20234 tgcl 21571 fgss2 22476 nmoid 23345 numclwwlkqhash 28148 chirredlem4 30164 pibt2 34692 lindsadd 34879 poimirlem28 34914 pridlc3 35345 stoweidlem34 42312 |
Copyright terms: Public domain | W3C validator |