![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mtoi | Structured version Visualization version Unicode version |
Description: Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |
Ref | Expression |
---|---|
mtoi.1 |
![]() ![]() ![]() |
mtoi.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mtoi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtoi.1 |
. . 3
![]() ![]() ![]() | |
2 | 1 | a1i 11 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | mtoi.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | mtod 181 |
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: mtbii 304 mtbiri 305 axc10 2095 pwnss 4567 eunex 4595 nsuceq0 5502 onssnel2i 5532 ssonprc 6616 reldmtpos 6978 dmtpos 6982 tfrlem15 7107 tz7.44-2 7122 tz7.48-3 7158 2pwuninel 7724 2pwne 7725 nnsdomg 7827 r111 8243 r1pwss 8252 wfelirr 8293 rankxplim3 8349 carduni 8412 pr2ne 8433 alephle 8516 alephfp 8536 pwcdadom 8643 cfsuc 8684 fin23lem28 8767 fin23lem30 8769 isfin1-2 8812 ac5b 8905 zorn2lem4 8926 zorn2lem7 8929 cfpwsdom 9006 nd1 9009 nd2 9010 canthp1 9076 pwfseqlem1 9080 gchhar 9101 winalim2 9118 ltxrlt 9701 recgt0 10446 nnunb 10862 indstr 11224 wrdlen2i 13014 rlimno1 13710 lcmfnncl 14595 isprm2 14625 nprmdvds1 14643 divgcdodd 14646 coprm 14650 ramtcl2 14959 ramtcl2OLD 14960 psgnunilem3 17130 torsubg 17485 prmcyg 17521 dprd2da 17668 prmirredlem 19057 pnfnei 20229 mnfnei 20230 1stccnp 20470 uzfbas 20906 ufinffr 20937 fin1aufil 20940 ovolunlem1a 22442 itg2gt0 22711 lgsquad2lem2 24280 dirith2 24359 usgranloop0 25100 nbgranself2 25157 frgra2v 25720 hon0 27439 ifeqeqx 28151 dfon2lem7 30428 soseq 30485 noseponlem 30548 nodenselem3 30565 nodenselem8 30570 bj-axc10v 31311 bj-eunex 31407 areacirclem4 32028 fdc 32067 dihglblem6 34902 pellexlem6 35672 pw2f1ocnv 35886 wepwsolem 35894 axc5c4c711toc5 36747 lptioo2 37705 lptioo1 37706 umgrnloop0 39183 usgrnloop0ALT 39274 1neven 39919 |
Copyright terms: Public domain | W3C validator |