Theorem pm2.65da 620

Description: Deduction rule for proof by contradiction. (Contributed by NM, 12-Jun-2014.)

Hypotheses

Ref	Expression
pm2.65da.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
pm2.65da.2	⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)

Assertion

Ref	Expression
pm2.65da	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem pm2.65da

Step	Hyp	Ref	Expression
1		pm2.65da.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 113	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.65da.2	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)
4	3	ex 113	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
5	2, 4	pm2.65d 619	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106  ax-in1 577  ax-in2 578

This theorem is referenced by:  condandc  809  nelrdva  2808  exmid01  3996  frirrg  4141  unsnfidcex  6557  unsnfidcel  6558  fodjuomnilem0  6707  exmidfodomrlemr  6731  exmidfodomrlemrALT  6732  prodgt0  8207  ixxdisj  9216  icodisj  9304  ltabs  10347  divalglemnqt  10700  zsupcllemstep  10721  infssuzex  10725  sqnprm  10897  znnen  10991  nnsn0  11238