![]() |
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 227 | . 2 ⊢ (𝜒 → 𝜓) |
4 | 1, 3 | nsyl 140 | 1 ⊢ (𝜑 → ¬ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: sylnibr 329 neqcomd 2734 ssnelpss 4103 fr3nr 7752 omopthi 8656 cofonr 8669 inf3lem6 9624 rankxpsuc 9873 cflim2 10254 ssfin4 10301 fin23lem30 10333 isf32lem5 10348 gchhar 10670 qextlt 13179 qextle 13180 fzneuz 13579 vdwnn 16930 psgnunilem3 19406 efgredlemb 19656 gsumzsplit 19837 lspexchn2 20972 lspindp2l 20975 lspindp2 20976 psrlidm 21833 mplcoe1 21902 mplcoe5 21905 ptopn2 23410 regr1lem2 23566 rnelfmlem 23778 hauspwpwf1 23813 tsmssplit 23978 reconn 24666 itg2splitlem 25600 itg2split 25601 itg2cn 25615 wilthlem2 26917 bposlem9 27141 2sqcoprm 27284 elntg2 28712 nfrgr2v 29994 hatomistici 32084 nn0min 32493 fedgmullem2 33194 qqhf 33455 hasheuni 33572 oddpwdc 33842 ballotlemimin 33993 ballotlemfrcn0 34017 bnj1388 34533 prv1n 34911 efrunt 35177 dfon2lem4 35253 dfon2lem7 35256 nandsym1 35797 atbase 38649 llnbase 38870 lplnbase 38895 lvolbase 38939 dalem48 39081 lhpbase 39359 cdlemg17pq 40033 cdlemg19 40045 cdlemg21 40047 dvh3dim3N 40810 rmspecnonsq 42134 setindtr 42252 flcidc 42405 omssrncard 42780 scotteld 43494 fmul01lt1lem2 44786 icccncfext 45088 stoweidlem14 45215 stoweidlem26 45227 stirlinglem5 45279 fourierdlem42 45350 fourierdlem62 45369 fourierdlem66 45373 hoicvr 45749 |
Copyright terms: Public domain | W3C validator |