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 1728 gencl 2586 spsbc 2775 eqsbc3r 2819 ssnelpss 3289 prexgOLD 3946 prexg 3947 posng 4412 sosng 4413 optocl 4416 relcnvexb 4857 funimass1 4976 dmfex 5079 f1ocnvb 5140 eqfnfv2 5266 elpreima 5286 dff13 5407 f1ocnvfv 5419 f1ocnvfvb 5420 fliftfun 5436 eusvobj2 5498 mpt2xopn0yelv 5854 rntpos 5872 erexb 6131 findcard2 6346 findcard2s 6347 enq0tr 6532 addnqprllem 6625 addnqprulem 6626 distrlem1prl 6680 distrlem1pru 6681 recexprlem1ssl 6731 recexprlem1ssu 6732 elrealeu 6906 addcan 7191 addcan2 7192 neg11 7262 negreb 7276 mulcanapd 7642 receuap 7650 cju 7913 nn1suc 7933 nnaddcl 7934 nndivtr 7955 znegclb 8278 zaddcllempos 8282 zmulcl 8297 zeo 8343 uz11 8495 uzp1 8506 eqreznegel 8549 xneg11 8747 frec2uzltd 9189 cj11 9505 rennim 9600 resqrexlemgt0 9618 bj-prexg 10031 strcollnft 10109 |
Copyright terms: Public domain | W3C validator |