![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl3an2 | GIF version |
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
Ref | Expression |
---|---|
syl3an2.1 | ⊢ (𝜑 → 𝜒) |
syl3an2.2 | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
syl3an2 | ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3an2.1 | . . 3 ⊢ (𝜑 → 𝜒) | |
2 | syl3an2.2 | . . . 4 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
3 | 2 | 3exp 1204 | . . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) |
4 | 1, 3 | syl5 32 | . 2 ⊢ (𝜓 → (𝜑 → (𝜃 → 𝜏))) |
5 | 4 | 3imp 1195 | 1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 980 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: syl3an2b 1286 syl3an2br 1289 syl3anl2 1298 nndi 6506 nnmass 6507 prarloclemarch2 7443 1idprl 7614 1idpru 7615 recexprlem1ssl 7657 recexprlem1ssu 7658 msqge0 8598 mulge0 8601 divsubdirap 8690 divdiv32ap 8702 peano2uz 9608 fzoshftral 10263 expdivap 10597 bcval5 10770 redivap 10910 imdivap 10917 absdiflt 11128 absdifle 11129 retanclap 11757 tannegap 11763 lcmgcdeq 12110 isprm3 12145 prmdvdsexpb 12176 dvdsprmpweqnn 12363 mulgaddcomlem 13078 mulginvcom 13080 cnpf2 14144 blres 14371 |
Copyright terms: Public domain | W3C validator |