Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mtbii | Structured version Visualization version Unicode version |
Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995.) |
Ref | Expression |
---|---|
mtbii.min | |
mtbii.maj |
Ref | Expression |
---|---|
mtbii |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtbii.min | . 2 | |
2 | mtbii.maj | . . 3 | |
3 | 2 | biimprd 238 | . 2 |
4 | 1, 3 | mtoi 190 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wb 196 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 |
This theorem is referenced by: limom 7080 omopthlem2 7736 fineqv 8175 dfac2 8953 nd3 9411 axunndlem1 9417 axregndlem1 9424 axregndlem2 9425 axregnd 9426 axacndlem5 9433 canthp1lem2 9475 alephgch 9496 inatsk 9600 addnidpi 9723 indpi 9729 archnq 9802 fsumsplit 14471 sumsplit 14499 geoisum1c 14611 fprodm1 14697 m1dvdsndvds 15503 gexdvds 17999 chtub 24937 wlkp1lem6 26575 avril1 27319 ballotlemi1 30564 ballotlemii 30565 distel 31709 nolt02o 31845 onsucsuccmpi 32442 bj-inftyexpidisj 33097 poimirlem28 33437 poimirlem32 33441 nvelim 41200 0nodd 41810 2nodd 41812 |
Copyright terms: Public domain | W3C validator |