![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > mto | Unicode version |
Description: The rule of modus
tollens. The rule says, "if ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mto.1 |
![]() ![]() ![]() |
mto.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mto |
![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mto.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | mto.1 |
. . 3
![]() ![]() ![]() | |
3 | 2 | a1i 10 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | pm2.65i 165 |
1
![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem is referenced by: mt3 171 mtbi 289 pm3.2ni 827 intnan 880 intnanr 881 equidOLD 1677 nexr 1760 equidqe 2173 ru 3045 neldifsn 3841 0cnsuc 4401 vinf 4555 0cnelphi 4597 proj1op 4600 proj2op 4601 xp0r 4842 xpnedisj 5513 epprc 5827 nenpw1pwlem2 6085 2p1e3c 6156 ncvsq 6256 0lt1c 6258 nchoice 6308 vncan 6337 |
Copyright terms: Public domain | W3C validator |