![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nsyl2 | Structured version Visualization version Unicode 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 129 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem is referenced by: con1i 133 con4i 134 oprcl 4190 ovrcl 6321 tfi 6677 limom 6704 oaabs2 7343 ecexr 7365 elpmi 7487 elmapex 7489 pmresg 7496 pmsspw 7503 ixpssmap2g 7548 ixpssmapg 7549 resixpfo 7557 infensuc 7747 pm54.43lem 8430 alephnbtwn 8499 cfpwsdom 9006 elbasfv 15163 elbasov 15164 restsspw 15323 homarcl 15916 isipodrs 16400 grpidval 16496 efgrelexlema 17392 subcmn 17470 dvdsrval 17866 mvrf1 18642 pf1rcl 18930 elocv 19224 matrcl 19430 restrcl 20166 ssrest 20185 iscnp2 20248 isfcls 21017 isnghm 21721 isnghmOLD 21739 dchrrcl 24161 eleenn 24919 hmdmadj 27586 indispcon 29950 cvmtop1 29976 cvmtop2 29977 mrsub0 30147 mrsubf 30148 mrsubccat 30149 mrsubcn 30150 mrsubco 30152 mrsubvrs 30153 msubf 30163 mclsrcl 30192 dfon2lem7 30428 sltval2 30536 sltres 30544 funpartlem 30702 rankeq1o 30931 atbase 32849 llnbase 33068 lplnbase 33093 lvolbase 33137 lhpbase 33557 mapco2g 35550 |
Copyright terms: Public domain | W3C validator |