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 140 | . 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 149 oprcl 4821 epelg 5459 elfvdm 6695 ovrcl 7186 tfi 7557 limom 7584 oaabs2 8261 ecexr 8283 elpmi 8414 elmapex 8416 pmresg 8423 pmsspw 8430 ixpssmap2g 8479 ixpssmapg 8480 resixpfo 8488 infensuc 8683 pm54.43lem 9416 alephnbtwn 9485 cfpwsdom 9994 elbasfv 16532 elbasov 16533 restsspw 16693 homarcl 17276 isipodrs 17759 grpidval 17859 efgrelexlema 18804 subcmn 18886 dvdsrval 19324 mvrf1 20133 pf1rcl 20440 elocv 20740 matrcl 20949 restrcl 21693 ssrest 21712 iscnp2 21775 isfcls 22545 isnghm 23259 dchrrcl 25743 clwwlknnn 27738 hmdmadj 29644 indispconn 32378 cvmtop1 32404 cvmtop2 32405 mrsub0 32660 mrsubf 32661 mrsubccat 32662 mrsubcn 32663 mrsubco 32665 mrsubvrs 32666 msubf 32676 mclsrcl 32705 dfon2lem7 32931 sltval2 33060 sltres 33066 funpartlem 33300 rankeq1o 33529 bj-brrelex12ALT 34253 bj-fvimacnv0 34456 atbase 36305 llnbase 36525 lplnbase 36550 lvolbase 36594 lhpbase 37014 mapco2g 39189 |
Copyright terms: Public domain | W3C validator |