![]() |
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 397 |
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 206 df-an 398 |
This theorem is referenced by: adantrrl 723 adantrrr 724 unfi 9172 isfin7-2 10391 mulsub 11657 fzsubel 13537 expsub 14076 ramlb 16952 0ram 16953 ressmplvsca 21586 tgcl 22472 fgss2 23378 nmoid 24259 madebdaylemlrcut 27394 numclwwlkqhash 29659 chirredlem4 31677 pibt2 36346 lindsadd 36529 poimirlem28 36564 pridlc3 36989 stoweidlem34 44798 |
Copyright terms: Public domain | W3C validator |