![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl3an | GIF version |
Description: A triple syllogism inference. (Contributed by NM, 13-May-2004.) |
Ref | Expression |
---|---|
syl3an.1 | ⊢ (𝜑 → 𝜓) |
syl3an.2 | ⊢ (𝜒 → 𝜃) |
syl3an.3 | ⊢ (𝜏 → 𝜂) |
syl3an.4 | ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) |
Ref | Expression |
---|---|
syl3an | ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3an.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | syl3an.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
3 | syl3an.3 | . . 3 ⊢ (𝜏 → 𝜂) | |
4 | 1, 2, 3 | 3anim123i 1129 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂)) |
5 | syl3an.4 | . 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) | |
6 | 4, 5 | syl 14 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 925 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 927 |
This theorem is referenced by: syl2an3an 1235 funtpg 5080 ftpg 5497 eloprabga 5751 prfidisj 6693 addasspig 6952 mulasspig 6954 distrpig 6955 addcanpig 6956 mulcanpig 6957 ltapig 6960 distrnqg 7009 distrnq0 7081 cnegexlem2 7721 zletr 8862 zdivadd 8898 iooneg 9468 zltaddlt1le 9486 fzen 9520 fzaddel 9536 fzrev 9561 fzrevral2 9583 fzshftral 9585 fzosubel2 9669 fzonn0p1p1 9687 resqrexlemover 10506 fisum0diag2 10904 dvdsnegb 11154 muldvds1 11162 muldvds2 11163 dvdscmul 11164 dvdsmulc 11165 dvds2add 11171 dvds2sub 11172 dvdstr 11174 addmodlteqALT 11201 divalgb 11266 ndvdsadd 11272 absmulgcd 11347 rpmulgcd 11356 cncongr2 11427 hashdvds 11538 |
Copyright terms: Public domain | W3C validator |