![]() |
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.) |
Ref | Expression |
---|---|
nsyl2.1 | ⊢ (𝜑 → ¬ 𝜓) |
nsyl2.2 | ⊢ (¬ 𝜒 → 𝜓) |
Ref | Expression |
---|---|
nsyl2 | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nsyl2.1 | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
2 | nsyl2.2 | . . 3 ⊢ (¬ 𝜒 → 𝜓) | |
3 | 2 | a1i 11 | . 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜓)) |
4 | 1, 3 | mt3d 142 | 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 146 oprcl 4566 ovrcl 6832 tfi 7201 limom 7228 oaabs2 7880 ecexr 7902 elpmi 8029 elmapex 8031 pmresg 8038 pmsspw 8045 ixpssmap2g 8092 ixpssmapg 8093 resixpfo 8101 infensuc 8295 pm54.43lem 9026 alephnbtwn 9095 cfpwsdom 9609 elbasfv 16128 elbasov 16129 restsspw 16301 homarcl 16886 isipodrs 17370 grpidval 17469 efgrelexlema 18370 subcmn 18450 dvdsrval 18854 mvrf1 19641 pf1rcl 19929 elocv 20230 matrcl 20436 restrcl 21183 ssrest 21202 iscnp2 21265 isfcls 22034 isnghm 22748 dchrrcl 25187 eleenn 25998 clwwlknnn 27189 hmdmadj 29140 indispconn 31555 cvmtop1 31581 cvmtop2 31582 mrsub0 31752 mrsubf 31753 mrsubccat 31754 mrsubcn 31755 mrsubco 31757 mrsubvrs 31758 msubf 31768 mclsrcl 31797 dfon2lem7 32031 sltval2 32147 sltres 32153 funpartlem 32387 rankeq1o 32616 atbase 35099 llnbase 35318 lplnbase 35343 lvolbase 35387 lhpbase 35807 mapco2g 37804 |
Copyright terms: Public domain | W3C validator |