![]() |
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 196 |
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 197 |
This theorem is referenced by: sylnibr 318 ssnelpss 3858 fr3nr 7142 omopthi 7904 inf3lem6 8701 rankxpsuc 8916 cflim2 9275 ssfin4 9322 fin23lem30 9354 isf32lem5 9369 gchhar 9691 qextlt 12225 qextle 12226 fzneuz 12612 vdwnn 15902 psgnunilem3 18114 efgredlemb 18357 gsumzsplit 18525 lspexchn2 19331 lspindp2l 19334 lspindp2 19335 psrlidm 19603 mplcoe1 19665 mplcoe5 19668 evlslem1 19715 ptopn2 21587 regr1lem2 21743 rnelfmlem 21955 hauspwpwf1 21990 tsmssplit 22154 reconn 22830 itg2splitlem 23712 itg2split 23713 itg2cn 23727 wilthlem2 24992 bposlem9 25214 nfrgr2v 27424 hatomistici 29528 nn0min 29874 2sqcoprm 29954 qqhf 30337 hasheuni 30454 oddpwdc 30723 ballotlemimin 30874 ballotlemfrcn0 30898 bnj1388 31406 efrunt 31895 dfon2lem4 31994 dfon2lem7 31997 nandsym1 32725 atbase 35077 llnbase 35296 lplnbase 35321 lvolbase 35365 dalem48 35507 lhpbase 35785 cdlemg17pq 36460 cdlemg19 36472 cdlemg21 36474 dvh3dim3N 37238 rmspecnonsq 37972 setindtr 38091 flcidc 38244 fmul01lt1lem2 40318 icccncfext 40601 stoweidlem14 40732 stoweidlem26 40744 stirlinglem5 40796 fourierdlem42 40867 fourierdlem62 40886 fourierdlem66 40890 hoicvr 41266 |
Copyright terms: Public domain | W3C validator |