Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nsyli | Structured version Visualization version GIF version |
Description: A negated syllogism inference. (Contributed by NM, 3-May-1994.) |
Ref | Expression |
---|---|
nsyli.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
nsyli.2 | ⊢ (𝜃 → ¬ 𝜒) |
Ref | Expression |
---|---|
nsyli | ⊢ (𝜑 → (𝜃 → ¬ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nsyli.2 | . 2 ⊢ (𝜃 → ¬ 𝜒) | |
2 | nsyli.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 2 | con3d 155 | . 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
4 | 1, 3 | syl5 34 | 1 ⊢ (𝜑 → (𝜃 → ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem is referenced by: necon3ad 3032 tz7.7 6220 onssneli 6303 tz7.48-2 8081 tz7.49 8084 php 8704 nndomo 8715 elirrv 9063 setind 9179 zorn2lem3 9923 alephval2 9997 inar1 10200 dfon2lem6 33037 sltres 33173 finminlem 33670 onint1 33801 poimirlem4 34900 nndomog 39903 gneispace 40490 |
Copyright terms: Public domain | W3C validator |