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 1396 disjiun 3993 tfrlem1 6299 tfrcl 6355 mkvprop 7146 ccfunen 7238 caucvgprprlemval 7662 suplocsrlem 7782 peano5uzti 9332 zfz1iso 10788 lcmneg 12040 prmind2 12086 pcfac 12314 cnmpt12 13280 cnmpt22 13287 limccnp2lem 13638 2sqlem6 13949 2sqlem8 13952 sbthom 14257 |
Copyright terms: Public domain | W3C validator |