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 GIF version

Theorem pm2.65ni 42481

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 193	. 2 ⊢ ¬ ¬ 𝜑
4	3	notnotri 131	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)