ferio - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > ferio		Unicode version

Theorem ferio 2304

Description: "Ferio" ("Ferioque"), one of the syllogisms of Aristotelian logic. No

, and some

, therefore some

is not

. (In Aristotelian notation, EIO-1: MeP and SiM therefore SoP.) For example, given "No homework is fun" and "Some reading is homework", therefore "Some reading is not fun". This is essentially a logical axiom in Aristotelian logic. Example from https://en.wikipedia.org/wiki/Syllogism. (Contributed by David A. Wheeler, 24-Aug-2016.) (Revised by David A. Wheeler, 2-Sep-2016.)

**Hypotheses**
Ref	Expression
ferio.maj
ferio.min	$/\$

**Assertion**
Ref	Expression
ferio	$/\$

**Proof of Theorem ferio**
Step	Hyp	Ref	Expression
1		ferio.maj	. 2
2		ferio.min	. 2 $/\$
3	1, 2	darii 2303	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 358

wal 1540

wex 1541

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-11 1746

This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542

This theorem is referenced by: (None)

W3C validator