aibnbna - Mathbox for Jarvin Udandy

	Mathbox for Jarvin Udandy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > aibnbna		Structured version Visualization version Unicode version

Theorem aibnbna 41073

Description: Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.)

**Hypotheses**
Ref	Expression
aibnbna.1
aibnbna.2

**Assertion**
Ref	Expression
aibnbna

**Proof of Theorem aibnbna**
Step	Hyp	Ref	Expression
1		aibnbna.2	. 2
2		aibnbna.1	. 2
3	1, 2	mto 188	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: aibnbaif 41074