| 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 228 | . 2 ⊢ (𝜒 → 𝜓) |
| 4 | 1, 3 | nsyl 140 | 1 ⊢ (𝜑 → ¬ 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: sylnibr 329 neqcomd 2747 ssnelpss 4114 fr3nr 7792 omopthi 8699 cofonr 8712 inf3lem6 9673 rankxpsuc 9922 cflim2 10303 ssfin4 10350 fin23lem30 10382 isf32lem5 10397 gchhar 10719 qextlt 13245 qextle 13246 fzneuz 13648 vdwnn 17036 psgnunilem3 19514 efgredlemb 19764 gsumzsplit 19945 lspexchn2 21133 lspindp2l 21136 lspindp2 21137 psrlidm 21982 mplcoe1 22055 mplcoe5 22058 ptopn2 23592 regr1lem2 23748 rnelfmlem 23960 hauspwpwf1 23995 tsmssplit 24160 reconn 24850 itg2splitlem 25783 itg2split 25784 itg2cn 25798 wilthlem2 27112 bposlem9 27336 2sqcoprm 27479 elntg2 29000 nfrgr2v 30291 hatomistici 32381 nn0min 32822 ccatws1f1o 32936 fedgmullem2 33681 qqhf 33987 hasheuni 34086 oddpwdc 34356 ballotlemimin 34508 ballotlemfrcn0 34532 bnj1388 35047 prv1n 35436 efrunt 35713 dfon2lem4 35787 dfon2lem7 35790 nandsym1 36423 atbase 39290 llnbase 39511 lplnbase 39536 lvolbase 39580 dalem48 39722 lhpbase 40000 cdlemg17pq 40674 cdlemg19 40686 cdlemg21 40688 dvh3dim3N 41451 fimgmcyc 42544 rmspecnonsq 42918 setindtr 43036 flcidc 43182 omssrncard 43553 scotteld 44265 fmul01lt1lem2 45600 icccncfext 45902 stoweidlem14 46029 stoweidlem26 46041 stirlinglem5 46093 fourierdlem42 46164 fourierdlem62 46183 fourierdlem66 46187 hoicvr 46563 |
| Copyright terms: Public domain | W3C validator |