![]() |
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 4350 phpm 6864 diffisn 6892 tridc 6898 nnnninfeq 7125 pm54.43 7188 addcanprleml 7612 addcanprlemu 7613 iseqf1olemklt 10484 isprm5lem 12140 pw2dvdseulemle 12166 sqne2sq 12176 pythagtriplem4 12267 pythagtriplem11 12273 pythagtriplem13 12275 ctinfomlemom 12427 ivthinc 14091 pwle2 14718 |
Copyright terms: Public domain | W3C validator |