| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > syl3c | GIF version | ||
| Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 7-Jul-2011.) |
| Ref | Expression |
|---|---|
| syl3c.1 | ⊢ (𝜑 → 𝜓) |
| syl3c.2 | ⊢ (𝜑 → 𝜒) |
| syl3c.3 | ⊢ (𝜑 → 𝜃) |
| syl3c.4 | ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) |
| Ref | Expression |
|---|---|
| syl3c | ⊢ (𝜑 → 𝜏) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syl3c.3 | . 2 ⊢ (𝜑 → 𝜃) | |
| 2 | syl3c.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
| 3 | syl3c.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
| 4 | syl3c.4 | . . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) | |
| 5 | 2, 3, 4 | sylc 62 | . 2 ⊢ (𝜑 → (𝜃 → 𝜏)) |
| 6 | 1, 5 | mpd 13 | 1 ⊢ (𝜑 → 𝜏) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
| This theorem is referenced by: bilukdc 1441 disjiun 4088 tfrlem1 6517 tfrcl 6573 mkvprop 7400 ccfunen 7526 caucvgprprlemval 7951 suplocsrlem 8071 peano5uzti 9631 seqf1oglem2 10826 zfz1iso 11149 wrd2ind 11351 lcmneg 12707 prmind2 12753 pcfac 12984 cnmpt12 15078 cnmpt22 15085 limccnp2lem 15467 2sqlem6 15916 2sqlem8 15919 gropd 15965 grstructd2dom 15966 sbthom 16731 |
| Copyright terms: Public domain | W3C validator |