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 114 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
4 | 1, 3 | mtod 653 | 1 ⊢ (𝜑 → ¬ 𝜓) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 ax-in1 604 ax-in2 605 |
This theorem is referenced by: frirrg 4322 phpm 6822 diffisn 6850 tridc 6856 nnnninfeq 7083 pm54.43 7137 addcanprleml 7546 addcanprlemu 7547 iseqf1olemklt 10410 isprm5lem 12052 pw2dvdseulemle 12078 sqne2sq 12088 pythagtriplem4 12179 pythagtriplem11 12185 pythagtriplem13 12187 ctinfomlemom 12303 ivthinc 13168 pwle2 13719 |
Copyright terms: Public domain | W3C validator |