![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl6ib | GIF version |
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl6ib.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
syl6ib.2 | ⊢ (𝜒 ↔ 𝜃) |
Ref | Expression |
---|---|
syl6ib | ⊢ (𝜑 → (𝜓 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6ib.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | syl6ib.2 | . . 3 ⊢ (𝜒 ↔ 𝜃) | |
3 | 2 | biimpi 118 | . 2 ⊢ (𝜒 → 𝜃) |
4 | 1, 3 | syl6 33 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: 3imtr3g 202 exp4a 358 con2biddc 808 nfalt 1511 alexim 1577 19.36-1 1604 ax11ev 1750 equs5or 1752 necon2bd 2304 necon2d 2305 necon1bbiddc 2309 necon2abiddc 2312 necon2bbiddc 2313 necon4idc 2315 necon4ddc 2318 necon1bddc 2323 spc2gv 2689 spc3gv 2691 mo2icl 2772 reupick 3255 prneimg 3574 invdisj 3788 trin 3893 ordsucss 4256 eqbrrdva 4533 elreldm 4588 elres 4674 xp11m 4789 ssrnres 4793 opelf 5093 dffo4 5347 dftpos3 5911 tfr1onlemaccex 5997 tfrcllemaccex 6010 nnaordex 6166 swoer 6200 nneneq 6392 fnfi 6446 prarloclemlo 6746 genprndl 6773 genprndu 6774 cauappcvgprlemladdrl 6909 caucvgprlemladdrl 6930 caucvgsrlemoffres 7038 caucvgsr 7040 nntopi 7122 letr 7261 reapcotr 7765 apcotr 7774 mulext1 7779 lt2msq 8031 nneoor 8530 xrletr 8954 icoshft 9088 caucvgre 10005 absext 10087 rexico 10245 gcdeq0 10512 bj-inf2vnlem2 10924 |
Copyright terms: Public domain | W3C validator |