Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mtand | Unicode 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 4323 phpm 6823 diffisn 6851 tridc 6857 nnnninfeq 7084 pm54.43 7138 addcanprleml 7547 addcanprlemu 7548 iseqf1olemklt 10411 isprm5lem 12062 pw2dvdseulemle 12088 sqne2sq 12098 pythagtriplem4 12189 pythagtriplem11 12195 pythagtriplem13 12197 ctinfomlemom 12323 ivthinc 13188 pwle2 13740 |
Copyright terms: Public domain | W3C validator |