![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > mtbi | Unicode version |
Description: An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Oct-2012.) |
Ref | Expression |
---|---|
mtbi.1 |
![]() ![]() ![]() |
mtbi.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mtbi |
![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtbi.1 |
. 2
![]() ![]() ![]() | |
2 | mtbi.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | biimpri 198 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mto 169 |
1
![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem is referenced by: mtbir 291 mtp-xorOLD 1543 vprc 4301 vnex 4303 opthwiener 4418 harndom 7488 alephprc 7936 unialeph 7938 ndvdsi 12885 bitsfzo 12902 nprmi 13049 dec2dvds 13354 dec5dvds2 13356 mreexmrid 13823 sinhalfpilem 20327 ppi2i 20905 measvuni 24521 ballotlem2 24699 dfon2lem7 25359 sltval2 25524 axlowdimlem13 25797 onsucsuccmpi 26097 jm2.23 26957 bnj1224 28879 bnj1541 28933 bnj1311 29099 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 178 |
Copyright terms: Public domain | W3C validator |