Theorem rcp-NDNEGI2 219

Description: ¬ Introduction Recipe. †

Hypotheses

Ref	Expression
rcp-NDNEGI2.1	⊢ ((𝛾₁ ∧ 𝛾₂) → 𝜑)
rcp-NDNEGI2.2	⊢ ((𝛾₁ ∧ 𝛾₂) → ¬ 𝜑)

Assertion

Ref	Expression
rcp-NDNEGI2	⊢ (𝛾₁ → ¬ 𝛾₂)

Proof of Theorem rcp-NDNEGI2

Step	Hyp	Ref	Expression
1		rcp-NDNEGI2.1	. 2 ⊢ ((𝛾₁ ∧ 𝛾₂) → 𝜑)
2		rcp-NDNEGI2.2	. 2 ⊢ ((𝛾₁ ∧ 𝛾₂) → ¬ 𝜑)
3	1, 2	ndnegi-P3.3 168	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:  dnegi-P3.29  273  mt-P3.32a  291  nmt-P3.32b  294  andasim-P3.46-L1  354  andasim-P3.46-L2  355  norel-P4.2a  367  norer-P4.2b  370  nandil-P4.3a  373  nandir-P4.3b  375  nprofeliml-P4.6a  389  nprofelimr-P4.6b  391  falseprofeliml-P4.7a  393  falseprofelimr-P4.7b  395  dnegeint-P4.12  421  falsenegi-P4.18  432  imasandint-P4.33b  490  rcp-RAA2  516