con2d - brismu bridi

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

Theorem con2d 289

Description: A contrapositive deduction. (Contributed by la korvo, 1-Jan-2025.)

**Hypothesis**
Ref	Expression
con2d.1	⊢ ganai broda gi ganai brode gi naku brodi

**Assertion**
Ref	Expression
con2d	⊢ ganai broda gi ganai brodi gi naku brode

**Proof of Theorem con2d**
Step	Hyp	Ref	Expression
1		con2d.1	. . . 4 ⊢ ganai broda gi ganai brode gi naku brodi
2		ax-efq 284	. . . 4 ⊢ ganai naku brodi gi ganai brodi gi naku brode
3	1, 2	syl6 25	. . 3 ⊢ ganai broda gi ganai brode gi ganai brodi gi naku brode
4	3	ganai-swap23 43	. 2 ⊢ ganai broda gi ganai brodi gi ganai brode gi naku brode
5		ax-sdo 281	. 2 ⊢ ganai ganai brode gi naku brode gi naku brode
6	4, 5	syl6 25	1 ⊢ ganai broda gi ganai brodi gi naku brode

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: mt2d 290