|   | 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 152 | . 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 2952 tz7.7 6409 onssneli 6499 tz7.48-2 8483 tz7.49 8486 php 9248 phpOLD 9260 nndomogOLD 9264 elirrv 9637 setind 9775 zorn2lem3 10539 alephval2 10613 inar1 10816 sltres 27708 dfon2lem6 35790 finminlem 36320 onint1 36451 poimirlem4 37632 ordnexbtwnsuc 43285 gneispace 44152 | 
| Copyright terms: Public domain | W3C validator |