![]() |
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 316 | 1 ⊢ (𝜑 → ¬ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 |
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 199 |
This theorem is referenced by: sylnibr 321 ssnelpss 3979 fr3nr 7310 omopthi 8084 inf3lem6 8890 rankxpsuc 9105 cflim2 9483 ssfin4 9530 fin23lem30 9562 isf32lem5 9577 gchhar 9899 qextlt 12413 qextle 12414 fzneuz 12804 vdwnn 16190 psgnunilem3 18386 efgredlemb 18631 gsumzsplit 18800 lspexchn2 19625 lspindp2l 19628 lspindp2 19629 psrlidm 19897 mplcoe1 19959 mplcoe5 19962 evlslem1 20008 ptopn2 21896 regr1lem2 22052 rnelfmlem 22264 hauspwpwf1 22299 tsmssplit 22463 reconn 23139 itg2splitlem 24052 itg2split 24053 itg2cn 24067 wilthlem2 25348 bposlem9 25570 2sqcoprm 25713 elntg2 26474 nfrgr2v 27806 hatomistici 29920 nn0min 30283 cycpm2tr 30448 fedgmullem2 30652 qqhf 30868 hasheuni 30985 oddpwdc 31254 ballotlemimin 31406 ballotlemfrcn0 31430 bnj1388 31947 efrunt 32456 dfon2lem4 32548 dfon2lem7 32551 nandsym1 33287 atbase 35867 llnbase 36087 lplnbase 36112 lvolbase 36156 dalem48 36298 lhpbase 36576 cdlemg17pq 37250 cdlemg19 37262 cdlemg21 37264 dvh3dim3N 38027 rmspecnonsq 38897 setindtr 39014 flcidc 39167 neqcomd 39918 scotteld 39954 fmul01lt1lem2 41295 icccncfext 41598 stoweidlem14 41728 stoweidlem26 41740 stirlinglem5 41792 fourierdlem42 41863 fourierdlem62 41882 fourierdlem66 41886 hoicvr 42259 |
Copyright terms: Public domain | W3C validator |