Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sylnib | Structured version Visualization version GIF version |
Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.) |
Ref | Expression |
---|---|
sylnib.1 | ⊢ (𝜑 → ¬ 𝜓) |
sylnib.2 | ⊢ (𝜓 ↔ 𝜒) |
Ref | Expression |
---|---|
sylnib | ⊢ (𝜑 → ¬ 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylnib.1 | . 2 ⊢ (𝜑 → ¬ 𝜓) | |
2 | sylnib.2 | . . 3 ⊢ (𝜓 ↔ 𝜒) | |
3 | 2 | a1i 11 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
4 | 1, 3 | mtbid 313 | 1 ⊢ (𝜑 → ¬ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 196 |
This theorem is referenced by: sylnibr 318 ssnelpss 3680 fr3nr 6871 omopthi 7624 inf3lem6 8413 rankxpsuc 8628 cflim2 8968 ssfin4 9015 fin23lem30 9047 isf32lem5 9062 gchhar 9380 qextlt 11908 qextle 11909 fzneuz 12290 vdwnn 15540 psgnunilem3 17739 efgredlemb 17982 gsumzsplit 18150 lspexchn2 18952 lspindp2l 18955 lspindp2 18956 psrlidm 19224 mplcoe1 19286 mplcoe5 19289 evlslem1 19336 ptopn2 21197 regr1lem2 21353 rnelfmlem 21566 hauspwpwf1 21601 tsmssplit 21765 reconn 22439 itg2splitlem 23321 itg2split 23322 itg2cn 23336 wilthlem2 24595 bposlem9 24817 frgra2v 26526 hatomistici 28605 nn0min 28954 2sqcoprm 28978 qqhf 29358 hasheuni 29474 oddpwdc 29743 ballotlemimin 29894 ballotlemfrcn0 29918 bnj1388 30355 efrunt 30844 dfon2lem4 30935 dfon2lem7 30938 nofulllem5 31105 nandsym1 31591 atbase 33594 llnbase 33813 lplnbase 33838 lvolbase 33882 dalem48 34024 lhpbase 34302 cdlemg17pq 34978 cdlemg19 34990 cdlemg21 34992 dvh3dim3N 35756 rmspecnonsq 36490 setindtr 36609 flcidc 36763 fmul01lt1lem2 38652 icccncfext 38773 stoweidlem14 38907 stoweidlem26 38919 stirlinglem5 38971 fourierdlem42 39042 fourierdlem62 39061 fourierdlem66 39065 hoicvr 39438 nfrgr2v 41442 |
Copyright terms: Public domain | W3C validator |