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 857 pm5.11dc 904 ax16i 1851 mor 2061 ceqsalg 2758 cgsexg 2765 cgsex2g 2766 cgsex4g 2767 spc2egv 2820 spc2gv 2821 spc3egv 2822 spc3gv 2823 disjne 3467 uneqdifeqim 3499 eqifdc 3559 triun 4098 sucssel 4407 ordsucg 4484 regexmidlem1 4515 relresfld 5138 relcoi1 5140 fornex 6092 f1dmex 6093 dom2d 6748 findcard 6863 nneo 9304 zeo2 9307 uznfz 10048 difelfzle 10079 ssfzo12 10169 facndiv 10662 fisumcom2 11390 fprodssdc 11542 fprodcom2fi 11578 ndvdssub 11878 bezoutlembi 11949 eucalglt 12000 prmind2 12063 coprm 12087 prmdiveq 12179 mhmlin 12679 inopn 12756 basis1 12800 tgss 12818 tgcl 12819 xmeteq0 13114 blssexps 13184 blssex 13185 mopni3 13239 neibl 13246 metss 13249 metcnp3 13266 logbgcd1irr 13640 bj-indsuc 13925 bj-nntrans 13948 |
Copyright terms: Public domain | W3C validator |