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 139 | 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 143 con4iOLD 144 oprcl 4365 ovrcl 6584 tfi 6945 limom 6972 oaabs2 7612 ecexr 7634 elpmi 7762 elmapex 7764 pmresg 7771 pmsspw 7778 ixpssmap2g 7823 ixpssmapg 7824 resixpfo 7832 infensuc 8023 pm54.43lem 8708 alephnbtwn 8777 cfpwsdom 9285 elbasfv 15748 elbasov 15749 restsspw 15915 homarcl 16501 isipodrs 16984 grpidval 17083 efgrelexlema 17985 subcmn 18065 dvdsrval 18468 mvrf1 19246 pf1rcl 19534 elocv 19831 matrcl 20037 restrcl 20771 ssrest 20790 iscnp2 20853 isfcls 21623 isnghm 22337 dchrrcl 24765 eleenn 25576 hmdmadj 28183 indispcon 30470 cvmtop1 30496 cvmtop2 30497 mrsub0 30667 mrsubf 30668 mrsubccat 30669 mrsubcn 30670 mrsubco 30672 mrsubvrs 30673 msubf 30683 mclsrcl 30712 dfon2lem7 30938 sltval2 31053 sltres 31061 funpartlem 31219 rankeq1o 31448 atbase 33594 llnbase 33813 lplnbase 33838 lvolbase 33882 lhpbase 34302 mapco2g 36295 |
Copyright terms: Public domain | W3C validator |