![]() |
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 9210 isfin7-2 10434 mulsub 11704 fzsubel 13597 expsub 14148 ramlb 17053 0ram 17054 ressmplvsca 22067 tgcl 22992 fgss2 23898 nmoid 24779 madebdaylemlrcut 27952 numclwwlkqhash 30404 chirredlem4 32422 pibt2 37400 lindsadd 37600 poimirlem28 37635 pridlc3 38060 stoweidlem34 45990 |
Copyright terms: Public domain | W3C validator |