![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm2.65da | GIF version |
Description: Deduction rule for proof by contradiction. (Contributed by NM, 12-Jun-2014.) |
Ref | Expression |
---|---|
pm2.65da.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
pm2.65da.2 | ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒) |
Ref | Expression |
---|---|
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 ⊢ (𝜑 → ¬ 𝜓) |
Colors of variables: wff set class |
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 |
Copyright terms: Public domain | W3C validator |