Theorem pm2.65da 622

Description: Deduction 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 621	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 579  ax-in2 580

This theorem is referenced by:  condandc  813  nelrdva  2820  exmid01  4023  frirrg  4168  fimax2gtrilemstep  6596  unsnfidcex  6610  unsnfidcel  6611  fodjuomnilem0  6781  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  prodgt0  8285  ixxdisj  9290  icodisj  9378  iseqf1olemnab  9882  seq3f1olemqsumk  9893  ltabs  10485  divalglemnqt  11002  zsupcllemstep  11023  infssuzex  11027  sqnprm  11199  znnen  11293  peano3nninf  11543