![]() |
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 843 oplem1 881 3impexpbicom 1324 hband 1375 hb3and 1376 nfand 1457 nfimd 1474 equsexd 1614 euim 1965 mopick2 1980 2moswapdc 1987 necon3bd 2242 necon3d 2243 necon2ad 2256 necon1abiddc 2261 ralrimd 2391 rspcimedv 2652 2reuswapdc 2737 eqsbc3r 2813 ra5 2840 difin 3168 r19.2m 3303 tpid3g 3474 sssnm 3516 ssiun 3690 ssiun2 3691 sotricim 4051 sotritrieq 4053 tron 4085 ordsucss 4196 ordunisuc2r 4205 ordpwsucss 4243 dmcosseq 4546 relssres 4591 trin2 4659 ssrnres 4706 fnun 4948 f1oun 5089 ssimaex 5177 chfnrn 5221 dffo4 5258 dffo5 5259 isoselem 5402 fnoprabg 5544 poxp 5794 issmo2 5845 smores 5848 tfr0 5878 tfrlemibxssdm 5882 swoer 6070 qsss 6101 indpi 6326 recexprlemm 6596 recexprlemloc 6603 recexprlem1ssl 6605 recexprlem1ssu 6606 recexprlemss1l 6607 recexprlemss1u 6608 zmulcl 8073 indstr 8312 eluzdc 8323 icoshft 8628 fzouzsplit 8805 bj-omssind 9394 bj-om 9396 bj-inf2vnlem3 9432 bj-inf2vnlem4 9433 |
Copyright terms: Public domain | W3C validator |