Theorem ndnegi-P3.3 168

Description: Natural Deduction: '¬' Introduction Rule.

If an assumption leads to a contradiction, then we can discharge it and conclude its negation.

Hypotheses

Ref	Expression
ndnegi-P3.3.1	⊢ ((𝛾 ∧ 𝜑) → 𝜓)
ndnegi-P3.3.2	⊢ ((𝛾 ∧ 𝜑) → ¬ 𝜓)

Assertion

Ref	Expression
ndnegi-P3.3	⊢ (𝛾 → ¬ 𝜑)

Proof of Theorem ndnegi-P3.3

Step	Hyp	Ref	Expression
1		ndnegi-P3.3.1	. . 3 ⊢ ((𝛾 ∧ 𝜑) → 𝜓)
2	1	export-P2.10b.SH 143	. 2 ⊢ (𝛾 → (𝜑 → 𝜓))
3		ndnegi-P3.3.2	. . 3 ⊢ ((𝛾 ∧ 𝜑) → ¬ 𝜓)
4	3	export-P2.10b.SH 143	. 2 ⊢ (𝛾 → (𝜑 → ¬ 𝜓))
5	2, 4	pfbycont-P1.16.AC.2SH 87	1 ⊢ (𝛾 → ¬ 𝜑)

Syntax hints:  ¬ wff-neg 9   → wff-imp 10   ∧ wff-and 132

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

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133

This theorem is referenced by:  rcp-NDNEGI1  218  rcp-NDNEGI2  219  rcp-NDNEGI3  220  rcp-NDNEGI4  221  rcp-NDNEGI5  222  raa-P4  514