![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl5com | GIF version |
Description: Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.) |
Ref | Expression |
---|---|
syl5com.1 | ⊢ (𝜑 → 𝜓) |
syl5com.2 | ⊢ (𝜒 → (𝜓 → 𝜃)) |
Ref | Expression |
---|---|
syl5com | ⊢ (𝜑 → (𝜒 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5com.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | a1d 22 | . 2 ⊢ (𝜑 → (𝜒 → 𝜓)) |
3 | syl5com.2 | . 2 ⊢ (𝜒 → (𝜓 → 𝜃)) | |
4 | 2, 3 | sylcom 28 | 1 ⊢ (𝜑 → (𝜒 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: com12 30 syl5 32 pm2.6dc 793 pm5.11dc 849 ax16i 1781 mor 1985 ceqsalg 2636 cgsexg 2643 cgsex2g 2644 cgsex4g 2645 spc2egv 2696 spc2gv 2697 spc3egv 2698 spc3gv 2699 disjne 3313 uneqdifeqim 3344 triun 3908 sucssel 4207 ordsucg 4274 regexmidlem1 4304 relresfld 4897 relcoi1 4899 fornex 5793 f1dmex 5794 dom2d 6341 findcard 6444 nneo 8583 zeo2 8586 uznfz 9248 difelfzle 9274 ssfzo12 9362 facndiv 9815 ndvdssub 10537 bezoutlembi 10601 eucalglt 10646 prmind2 10709 coprm 10730 bj-indsuc 10990 bj-nntrans 11013 |
Copyright terms: Public domain | W3C validator |