![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl5ib | GIF version |
Description: A mixed syllogism inference. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl5ib.1 | ⊢ (φ → ψ) |
syl5ib.2 | ⊢ (χ → (ψ ↔ θ)) |
Ref | Expression |
---|---|
syl5ib | ⊢ (χ → (φ → θ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5ib.1 | . 2 ⊢ (φ → ψ) | |
2 | syl5ib.2 | . . 3 ⊢ (χ → (ψ ↔ θ)) | |
3 | 2 | biimpd 132 | . 2 ⊢ (χ → (ψ → θ)) |
4 | 1, 3 | syl5 28 | 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: syl5ibcom 144 syl5ibr 145 sbft 1725 gencl 2580 spsbc 2769 eqsbc3r 2813 ssnelpss 3283 prexgOLD 3937 prexg 3938 posng 4355 sosng 4356 optocl 4359 relcnvexb 4800 funimass1 4919 dmfex 5022 f1ocnvb 5083 eqfnfv2 5209 elpreima 5229 dff13 5350 f1ocnvfv 5362 f1ocnvfvb 5363 fliftfun 5379 eusvobj2 5441 mpt2xopn0yelv 5795 rntpos 5813 erexb 6067 enq0tr 6417 addnqprllem 6510 addnqprulem 6511 distrlem1prl 6558 distrlem1pru 6559 recexprlem1ssl 6605 recexprlem1ssu 6606 addcan 6988 addcan2 6989 neg11 7058 negreb 7072 mulcanapd 7424 receuap 7432 cju 7694 nn1suc 7714 nnaddcl 7715 nndivtr 7736 znegclb 8054 zaddcllempos 8058 zmulcl 8073 zeo 8119 uz11 8271 uzp1 8282 eqreznegel 8325 xneg11 8517 frec2uzltd 8870 cj11 9133 rennim 9211 bj-prexg 9366 strcollnft 9444 |
Copyright terms: Public domain | W3C validator |