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-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: com12 30 syl5 32 pm2.6dc 847 pm5.11dc 894 ax16i 1830 mor 2041 ceqsalg 2714 cgsexg 2721 cgsex2g 2722 cgsex4g 2723 spc2egv 2775 spc2gv 2776 spc3egv 2777 spc3gv 2778 disjne 3416 uneqdifeqim 3448 eqifdc 3506 triun 4039 sucssel 4346 ordsucg 4418 regexmidlem1 4448 relresfld 5068 relcoi1 5070 fornex 6013 f1dmex 6014 dom2d 6667 findcard 6782 nneo 9154 zeo2 9157 uznfz 9883 difelfzle 9911 ssfzo12 10001 facndiv 10485 fisumcom2 11207 ndvdssub 11627 bezoutlembi 11693 eucalglt 11738 prmind2 11801 coprm 11822 inopn 12170 basis1 12214 tgss 12232 tgcl 12233 xmeteq0 12528 blssexps 12598 blssex 12599 mopni3 12653 neibl 12660 metss 12663 metcnp3 12680 bj-indsuc 13126 bj-nntrans 13149 |
Copyright terms: Public domain | W3C validator |