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 143 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
4 | 1, 3 | mtod 652 | 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-in1 603 ax-in2 604 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: eqneltrd 2235 neleqtrrd 2238 fidifsnen 6764 php5fin 6776 tridc 6793 fimax2gtrilemstep 6794 en2eqpr 6801 inflbti 6911 omp1eomlem 6979 difinfsnlem 6984 addnidpig 7144 nqnq0pi 7246 ltpopr 7403 cauappcvgprlemladdru 7464 caucvgprlemladdrl 7486 caucvgprprlemnkltj 7497 caucvgprprlemnkeqj 7498 caucvgprprlemaddq 7516 ltposr 7571 axpre-suploclemres 7709 axltirr 7831 reapirr 8339 apirr 8367 indstr2 9403 xrltnsym 9579 xrlttr 9581 xrltso 9582 xltadd1 9659 xposdif 9665 xleaddadd 9670 lbioog 9696 ubioog 9697 fzn 9822 flqltnz 10060 iseqf1olemnab 10261 iseqf1olemqk 10267 exp3val 10295 zfz1isolemiso 10582 xrmaxltsup 11027 binomlem 11252 dvdsle 11542 2tp1odd 11581 divalglemeuneg 11620 bezoutlemle 11696 rpexp 11831 oddpwdclemxy 11847 oddpwdclemndvds 11849 sqpweven 11853 2sqpwodd 11854 ctinfom 11941 ivthinc 12790 |
Copyright terms: Public domain | W3C validator |