Theorem ndnege-P3.4 169

Description: Natural Deduction: '¬' Elimination Rule.

If we can deduce a contradiction within some context, then we can deduce any arbitrary WFF from that same context.

Hypotheses

Ref	Expression
ndnege-P3.4.1	⊢ (𝛾 → 𝜑)
ndnege-P3.4.2	⊢ (𝛾 → ¬ 𝜑)

Assertion

Ref	Expression
ndnege-P3.4	⊢ (𝛾 → 𝜓)

Proof of Theorem ndnege-P3.4

Step	Hyp	Ref	Expression
1		ndnege-P3.4.1	. 2 ⊢ (𝛾 → 𝜑)
2		ndnege-P3.4.2	. 2 ⊢ (𝛾 → ¬ 𝜑)
3	1, 2	poe-P1.11b.AC.2SH 67	1 ⊢ (𝛾 → 𝜓)

Syntax hints:  ¬ wff-neg 9   → wff-imp 10

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14

This theorem is referenced by:  ndfalsei-P3.19  184  rcp-NDNEGE0  223  ndnege-P3.4.CL  243  dnege-P3.30  276  orasim-P3.48-L1  359  impoe-P4.4a  377  nimpoe-P4.4b  380  profeliml-P4.5a  385  profelimr-P4.5b  387  dmorgarev-L4.2  453