pm2.65ni - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > pm2.65ni		Structured version Visualization version Unicode version

Theorem pm2.65ni 39210

Description: Inference rule for proof by contradiction. (Contributed by Glauco Siliprandi, 5-Apr-2020.)

**Hypotheses**
Ref	Expression
pm2.65ni.1
pm2.65ni.2

**Assertion**
Ref	Expression
pm2.65ni

**Proof of Theorem pm2.65ni**
Step	Hyp	Ref	Expression
1		pm2.65ni.1	. . 3
2		pm2.65ni.2	. . 3
3	1, 2	pm2.65i 185	. 2
4	3	notnotri 126	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: (None)