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 1165 | . . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) |
4 | 1, 3 | syl5 32 | . 2 ⊢ (𝜓 → (𝜑 → (𝜃 → 𝜏))) |
5 | 4 | 3imp 1160 | 1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: syl3an2b 1238 syl3an2br 1241 syl3anl2 1250 nndi 6350 nnmass 6351 prarloclemarch2 7195 1idprl 7366 1idpru 7367 recexprlem1ssl 7409 recexprlem1ssu 7410 msqge0 8346 mulge0 8349 divsubdirap 8436 divdiv32ap 8448 peano2uz 9346 fzoshftral 9983 expdivap 10312 bcval5 10477 redivap 10614 imdivap 10621 absdiflt 10832 absdifle 10833 retanclap 11356 tannegap 11362 lcmgcdeq 11691 isprm3 11726 prmdvdsexpb 11754 cnpf2 12303 blres 12530 |
Copyright terms: Public domain | W3C validator |