![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mtbid | Unicode version |
Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.) |
Ref | Expression |
---|---|
mtbid.min |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
mtbid.maj |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mtbid |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtbid.min |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | mtbid.maj |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | biimprd 158 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mtod 664 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: sylnib 677 eqneltrrd 2286 neleqtrd 2287 eueq3dc 2926 efrirr 4368 fidcenumlemrks 6977 nqnq0pi 7462 zdclt 9355 xleaddadd 9912 frec2uzf1od 10432 expnegap0 10554 bcval5 10770 zfz1isolemiso 10846 seq3coll 10849 fisumss 11427 fprodssdc 11625 rpdvds 12126 oddpwdclemodd 12199 pceq0 12349 pcmpt 12370 lgseisenlem1 14887 2sqlem8a 14906 2sqlem8 14907 pwle2 15186 |
Copyright terms: Public domain | W3C validator |