![]() |
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 615 | . 2 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜃)) |
3 | sylanr2.2 | . 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
4 | 2, 3 | sylan2 591 | 1 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜑)) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 395 |
This theorem is referenced by: adantrrl 722 adantrrr 723 unfi 9197 isfin7-2 10421 mulsub 11689 fzsubel 13572 expsub 14111 ramlb 16991 0ram 16992 ressmplvsca 21991 tgcl 22916 fgss2 23822 nmoid 24703 madebdaylemlrcut 27871 numclwwlkqhash 30257 chirredlem4 32275 pibt2 37027 lindsadd 37217 poimirlem28 37252 pridlc3 37677 stoweidlem34 45560 |
Copyright terms: Public domain | W3C validator |