nsyl3 - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > nsyl3

Theorem nsyl3 291

Description: A negated syllogism. Can be seen as a deduction form of modus tollens. (Contributed by la korvo, 1-Jan-2025.)

**Hypotheses**
Ref	Expression
nsyl3.1	⊢ ganai broda gi naku brode
nsyl3.2	⊢ ganai brodi gi brode

**Assertion**
Ref	Expression
nsyl3	⊢ ganai brodi gi naku broda

**Proof of Theorem nsyl3**
Step	Hyp	Ref	Expression
1		nsyl3.2	. 2 ⊢ ganai brodi gi brode
2		nsyl3.1	. . 3 ⊢ ganai broda gi naku brode
3	2	ki 12	. 2 ⊢ ganai brodi gi ganai broda gi naku brode
4	1, 3	mt2d 290	1 ⊢ ganai brodi gi naku broda

Colors of variables: sumti selbri bridi

Syntax hints: ganai bgan 9 naku bnk 272

This theorem was proved from axioms: ax-mp 10 ax-k 11 ax-s 15 ax-sdo 281 ax-efq 284

This theorem is referenced by: con2i 292 nsyl 295