![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mtand | GIF version |
Description: A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.) |
Ref | Expression |
---|---|
mtand.1 | ⊢ (𝜑 → ¬ 𝜒) |
mtand.2 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
mtand | ⊢ (𝜑 → ¬ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtand.1 | . 2 ⊢ (𝜑 → ¬ 𝜒) | |
2 | mtand.2 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
3 | 2 | ex 115 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
4 | 1, 3 | mtod 663 | 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-ia3 108 ax-in1 614 ax-in2 615 |
This theorem is referenced by: frirrg 4352 phpm 6868 diffisn 6896 tridc 6902 nnnninfeq 7129 pm54.43 7192 addcanprleml 7616 addcanprlemu 7617 iseqf1olemklt 10488 isprm5lem 12144 pw2dvdseulemle 12170 sqne2sq 12180 pythagtriplem4 12271 pythagtriplem11 12277 pythagtriplem13 12279 ctinfomlemom 12431 lssvancl1 13465 ivthinc 14282 pwle2 14910 |
Copyright terms: Public domain | W3C validator |