![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl6ibr | GIF version |
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl6ibr.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
syl6ibr.2 | ⊢ (𝜃 ↔ 𝜒) |
Ref | Expression |
---|---|
syl6ibr | ⊢ (𝜑 → (𝜓 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6ibr.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | syl6ibr.2 | . . 3 ⊢ (𝜃 ↔ 𝜒) | |
3 | 2 | biimpri 124 | . 2 ⊢ (𝜒 → 𝜃) |
4 | 1, 3 | syl6 29 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 3imtr4g 194 imp4a 331 dcbi 844 oplem1 882 3impexpbicom 1327 hband 1378 hb3and 1379 nfand 1460 nfimd 1477 equsexd 1617 euim 1968 mopick2 1983 2moswapdc 1990 necon3bd 2248 necon3d 2249 necon2ad 2262 necon1abiddc 2267 ralrimd 2397 rspcimedv 2658 2reuswapdc 2743 eqsbc3r 2819 ra5 2846 difin 3174 r19.2m 3309 tpid3g 3483 sssnm 3525 ssiun 3699 ssiun2 3700 sotricim 4060 sotritrieq 4062 tron 4119 ordsucss 4230 ordunisuc2r 4240 ordpwsucss 4291 dmcosseq 4603 relssres 4648 trin2 4716 ssrnres 4763 fnun 5005 f1oun 5146 ssimaex 5234 chfnrn 5278 dffo4 5315 dffo5 5316 isoselem 5459 fnoprabg 5602 poxp 5853 issmo2 5904 smores 5907 tfr0 5937 tfrlemibxssdm 5941 swoer 6134 qsss 6165 findcard 6345 findcard2 6346 findcard2s 6347 indpi 6440 recexprlemm 6722 recexprlemloc 6729 recexprlem1ssl 6731 recexprlem1ssu 6732 recexprlemss1l 6733 recexprlemss1u 6734 zmulcl 8297 indstr 8536 eluzdc 8547 icoshft 8858 fzouzsplit 9035 sqrt2irr 9878 bj-omssind 10059 bj-om 10061 bj-inf2vnlem3 10097 bj-inf2vnlem4 10098 |
Copyright terms: Public domain | W3C validator |