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 637 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 588 ax-in2 589 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: sylnib 650 eqneltrrd 2214 neleqtrd 2215 eueq3dc 2831 efrirr 4245 fidcenumlemrks 6809 nqnq0pi 7214 zdclt 9096 xleaddadd 9638 frec2uzf1od 10147 expnegap0 10269 bcval5 10477 zfz1isolemiso 10550 seq3coll 10553 fisumss 11129 rpdvds 11707 oddpwdclemodd 11777 pwle2 13120 |
Copyright terms: Public domain | W3C validator |