![]() |
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 157 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mtod 635 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 586 ax-in2 587 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: sylnib 648 eqneltrrd 2211 neleqtrd 2212 eueq3dc 2827 efrirr 4235 fidcenumlemrks 6793 nqnq0pi 7194 zdclt 9032 xleaddadd 9563 frec2uzf1od 10072 expnegap0 10194 bcval5 10402 zfz1isolemiso 10475 seq3coll 10478 fisumss 11053 rpdvds 11626 oddpwdclemodd 11695 pwle2 12885 |
Copyright terms: Public domain | W3C validator |