![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl3an3 | GIF version |
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
Ref | Expression |
---|---|
syl3an3.1 | ⊢ (𝜑 → 𝜃) |
syl3an3.2 | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
syl3an3 | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3an3.1 | . . 3 ⊢ (𝜑 → 𝜃) | |
2 | syl3an3.2 | . . . 4 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
3 | 2 | 3exp 1143 | . . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) |
4 | 1, 3 | syl7 69 | . 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜏))) |
5 | 4 | 3imp 1138 | 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: syl3an3b 1213 syl3an3br 1216 vtoclgft 2670 ovmpt2x 5787 ovmpt2ga 5788 nnanq0 7078 apreim 8141 apsub1 8178 divassap 8218 ltmul2 8378 elfzo 9621 fzodcel 9624 subcn2 10761 mulcn2 10762 ndvdsp1 11271 gcddiv 11347 lcmneg 11395 |
Copyright terms: Public domain | W3C validator |