|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > nsyl2 | Structured version Visualization version GIF version | ||
| Description: A negated syllogism inference. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 14-Nov-2023.) | 
| Ref | Expression | 
|---|---|
| nsyl2.1 | ⊢ (𝜑 → ¬ 𝜓) | 
| nsyl2.2 | ⊢ (¬ 𝜒 → 𝜓) | 
| Ref | Expression | 
|---|---|
| nsyl2 | ⊢ (𝜑 → 𝜒) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | nsyl2.1 | . . 3 ⊢ (𝜑 → ¬ 𝜓) | |
| 2 | nsyl2.2 | . . 3 ⊢ (¬ 𝜒 → 𝜓) | |
| 3 | 1, 2 | nsyl3 138 | . 2 ⊢ (¬ 𝜒 → ¬ 𝜑) | 
| 4 | 3 | con4i 114 | 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: con1i 147 oprcl 4898 epelg 5584 elfvdm 6942 ovrcl 7473 elfvov1 7474 elfvov2 7475 tfi 7875 limom 7904 oaabs2 8688 ecexr 8751 elpmi 8887 elmapex 8889 pmresg 8911 pmsspw 8918 ixpssmap2g 8968 ixpssmapg 8969 resixpfo 8977 infensuc 9196 pm54.43lem 10041 alephnbtwn 10112 cfpwsdom 10625 elbasfv 17254 elbasov 17255 restsspw 17477 homarcl 18074 isipodrs 18583 grpidval 18675 efgrelexlema 19768 subcmn 19856 dvdsrval 20362 elocv 21687 mvrf1 22007 pf1rcl 22354 matrcl 22417 restrcl 23166 ssrest 23185 iscnp2 23248 isfcls 24018 isnghm 24745 dchrrcl 27285 sltval2 27702 sltres 27708 clwwlknnn 30053 hmdmadj 31960 indispconn 35240 cvmtop1 35266 cvmtop2 35267 mrsub0 35522 mrsubf 35523 mrsubccat 35524 mrsubcn 35525 mrsubco 35527 mrsubvrs 35528 msubf 35538 mclsrcl 35567 dfon2lem7 35791 funpartlem 35944 rankeq1o 36173 bj-brrelex12ALT 37069 bj-fvimacnv0 37288 atbase 39291 llnbase 39512 lplnbase 39537 lvolbase 39581 lhpbase 40001 mapco2g 42730 | 
| Copyright terms: Public domain | W3C validator |