![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > intnand | GIF version |
Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.) |
Ref | Expression |
---|---|
intnand.1 | ⊢ (𝜑 → ¬ 𝜓) |
Ref | Expression |
---|---|
intnand | ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | intnand.1 | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
2 | simpr 110 | . 2 ⊢ ((𝜒 ∧ 𝜓) → 𝜓) | |
3 | 1, 2 | nsyl 629 | 1 ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 107 ax-in1 615 ax-in2 616 |
This theorem is referenced by: dcan 934 poxp 6250 cauappcvgprlemladdrl 7673 caucvgprlemladdrl 7694 xrrebnd 9836 fzpreddisj 10088 fzp1nel 10121 fprodntrivap 11609 gcdsupex 11975 gcdsupcl 11976 gcdnncl 11985 gcd2n0cl 11987 qredeu 12114 cncongr2 12121 divnumden 12213 divdenle 12214 phisum 12257 pythagtriplem4 12285 pythagtriplem8 12289 pythagtriplem9 12290 isnsgrp 12834 ivthinclemdisj 14501 lgsneg 14808 |
Copyright terms: Public domain | W3C validator |