![]() |
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 143 | 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 4662 elfvdm 6478 ovrcl 6962 tfi 7331 limom 7358 oaabs2 8009 ecexr 8031 elpmi 8159 elmapex 8161 pmresg 8168 pmsspw 8175 ixpssmap2g 8223 ixpssmapg 8224 resixpfo 8232 infensuc 8426 pm54.43lem 9158 alephnbtwn 9227 cfpwsdom 9741 elbasfv 16316 elbasov 16317 restsspw 16478 homarcl 17063 isipodrs 17547 grpidval 17646 efgrelexlema 18548 subcmn 18628 dvdsrval 19032 mvrf1 19822 pf1rcl 20109 elocv 20411 matrcl 20622 restrcl 21369 ssrest 21388 iscnp2 21451 isfcls 22221 isnghm 22935 dchrrcl 25417 eleenn 26245 clwwlknnn 27422 hmdmadj 29371 indispconn 31815 cvmtop1 31841 cvmtop2 31842 mrsub0 32012 mrsubf 32013 mrsubccat 32014 mrsubcn 32015 mrsubco 32017 mrsubvrs 32018 msubf 32028 mclsrcl 32057 dfon2lem7 32282 sltval2 32398 sltres 32404 funpartlem 32638 rankeq1o 32867 atbase 35438 llnbase 35658 lplnbase 35683 lvolbase 35727 lhpbase 36147 mapco2g 38230 |
Copyright terms: Public domain | W3C validator |