![]() |
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 4351 phpm 6865 diffisn 6893 tridc 6899 nnnninfeq 7126 pm54.43 7189 addcanprleml 7613 addcanprlemu 7614 iseqf1olemklt 10485 isprm5lem 12141 pw2dvdseulemle 12167 sqne2sq 12177 pythagtriplem4 12268 pythagtriplem11 12274 pythagtriplem13 12276 ctinfomlemom 12428 ivthinc 14124 pwle2 14751 |
Copyright terms: Public domain | W3C validator |