![]() |
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 140 | 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 144 con4iOLD 145 oprcl 4459 ovrcl 6726 tfi 7095 limom 7122 oaabs2 7770 ecexr 7792 elpmi 7918 elmapex 7920 pmresg 7927 pmsspw 7934 ixpssmap2g 7979 ixpssmapg 7980 resixpfo 7988 infensuc 8179 pm54.43lem 8863 alephnbtwn 8932 cfpwsdom 9444 elbasfv 15967 elbasov 15968 restsspw 16139 homarcl 16725 isipodrs 17208 grpidval 17307 efgrelexlema 18208 subcmn 18288 dvdsrval 18691 mvrf1 19473 pf1rcl 19761 elocv 20060 matrcl 20266 restrcl 21009 ssrest 21028 iscnp2 21091 isfcls 21860 isnghm 22574 dchrrcl 25010 eleenn 25821 clwwlknnn 26995 hmdmadj 28927 indispconn 31342 cvmtop1 31368 cvmtop2 31369 mrsub0 31539 mrsubf 31540 mrsubccat 31541 mrsubcn 31542 mrsubco 31544 mrsubvrs 31545 msubf 31555 mclsrcl 31584 dfon2lem7 31818 sltval2 31934 sltres 31940 funpartlem 32174 rankeq1o 32403 atbase 34894 llnbase 35113 lplnbase 35138 lvolbase 35182 lhpbase 35602 mapco2g 37594 |
Copyright terms: Public domain | W3C validator |