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 | biimpri 229 | . 2 ⊢ (𝜒 → 𝜓) |
4 | 1, 3 | nsyl 142 | 1 ⊢ (𝜑 → ¬ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 |
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 208 |
This theorem is referenced by: sylnibr 330 neqcomd 2828 ssnelpss 4085 fr3nr 7483 omopthi 8273 inf3lem6 9084 rankxpsuc 9299 cflim2 9673 ssfin4 9720 fin23lem30 9752 isf32lem5 9767 gchhar 10089 qextlt 12584 qextle 12585 fzneuz 12976 vdwnn 16322 psgnunilem3 18553 efgredlemb 18801 gsumzsplit 18976 lspexchn2 19832 lspindp2l 19835 lspindp2 19836 psrlidm 20111 mplcoe1 20174 mplcoe5 20177 ptopn2 22120 regr1lem2 22276 rnelfmlem 22488 hauspwpwf1 22523 tsmssplit 22687 reconn 23363 itg2splitlem 24276 itg2split 24277 itg2cn 24291 wilthlem2 25573 bposlem9 25795 2sqcoprm 25938 elntg2 26698 nfrgr2v 27978 hatomistici 30066 nn0min 30463 fedgmullem2 30925 qqhf 31126 hasheuni 31243 oddpwdc 31511 ballotlemimin 31662 ballotlemfrcn0 31686 bnj1388 32202 prv1n 32575 efrunt 32836 dfon2lem4 32928 dfon2lem7 32931 nandsym1 33667 atbase 36305 llnbase 36525 lplnbase 36550 lvolbase 36594 dalem48 36736 lhpbase 37014 cdlemg17pq 37688 cdlemg19 37700 cdlemg21 37702 dvh3dim3N 38465 rmspecnonsq 39382 setindtr 39499 flcidc 39652 scotteld 40459 fmul01lt1lem2 41742 icccncfext 42046 stoweidlem14 42176 stoweidlem26 42188 stirlinglem5 42240 fourierdlem42 42311 fourierdlem62 42330 fourierdlem66 42334 hoicvr 42707 |
Copyright terms: Public domain | W3C validator |