Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mtbird | GIF version |
Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.) |
Ref | Expression |
---|---|
mtbird.min | ⊢ (𝜑 → ¬ 𝜒) |
mtbird.maj | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
mtbird | ⊢ (𝜑 → ¬ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtbird.min | . 2 ⊢ (𝜑 → ¬ 𝜒) | |
2 | mtbird.maj | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 2 | biimpd 142 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
4 | 1, 3 | mtod 621 | 1 ⊢ (𝜑 → ¬ 𝜓) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-in1 576 ax-in2 577 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: eqneltrd 2174 neleqtrrd 2177 fidifsnen 6355 php5fin 6366 en2eqpr 6380 inflbti 6437 addnidpig 6526 nqnq0pi 6628 ltpopr 6785 cauappcvgprlemladdru 6846 caucvgprlemladdrl 6868 caucvgprprlemnkltj 6879 caucvgprprlemnkeqj 6880 caucvgprprlemaddq 6898 ltposr 6940 axltirr 7179 reapirr 7677 apirr 7705 indstr2 8696 xrltnsym 8868 xrlttr 8870 xrltso 8871 lbioog 8936 ubioog 8937 fzn 9061 flqltnz 9289 expival 9478 dvdsle 10244 2tp1odd 10284 divalglemeuneg 10323 bezoutlemle 10397 rpexp 10532 oddpwdclemxy 10547 oddpwdclemndvds 10549 sqpweven 10553 2sqpwodd 10554 |
Copyright terms: Public domain | W3C validator |