![]() |
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 113 | . 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 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 3imtr3g 193 exp4a 348 con2biddc 773 nfalt 1467 alexim 1533 19.36-1 1560 ax11ev 1706 equs5or 1708 necon2bd 2257 necon2d 2258 necon1bbiddc 2262 necon2abiddc 2265 necon2bbiddc 2266 necon4idc 2268 necon4ddc 2271 necon1bddc 2276 spc2gv 2637 spc3gv 2639 mo2icl 2714 eqsbc3r 2813 reupick 3215 prneimg 3536 invdisj 3750 trin 3855 ordsucss 4196 eqbrrdva 4448 elreldm 4503 elres 4589 xp11m 4702 ssrnres 4706 opelf 5005 dffo4 5258 dftpos3 5818 tfr0 5878 nnaordex 6036 swoer 6070 prarloclemlo 6477 genprndl 6504 genprndu 6505 cauappcvgprlemladdrl 6629 caucvgprlemladdrl 6649 letr 6898 reapcotr 7382 apcotr 7391 mulext1 7396 lt2msq 7633 nneoor 8116 xrletr 8494 icoshft 8628 bj-inf2vnlem2 9431 |
Copyright terms: Public domain | W3C validator |