![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > intnanrd | GIF version |
Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.) |
Ref | Expression |
---|---|
intnand.1 | ⊢ (𝜑 → ¬ 𝜓) |
Ref | Expression |
---|---|
intnanrd | ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | intnand.1 | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
2 | simpl 109 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓) | |
3 | 1, 2 | nsyl 628 | 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-ia1 106 ax-in1 614 ax-in2 615 |
This theorem is referenced by: dcan 933 bianfd 948 frecabcl 6399 frecsuclem 6406 xrrebnd 9817 fzpreddisj 10068 iseqf1olemqk 10491 gcdsupex 11952 gcdsupcl 11953 nndvdslegcd 11960 divgcdnn 11970 sqgcd 12024 coprm 12138 pclemdc 12282 1arith 12359 ctiunctlemudc 12432 lgsval2lem 14304 lgsval4a 14316 lgsdilem 14321 |
Copyright terms: Public domain | W3C validator |