![]() |
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 1138 | . . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) |
4 | 1, 3 | syl5 32 | . 2 ⊢ (𝜓 → (𝜑 → (𝜃 → 𝜏))) |
5 | 4 | 3imp 1133 | 1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: syl3an2b 1207 syl3an2br 1210 syl3anl2 1219 nndi 6179 nnmass 6180 prarloclemarch2 6881 1idprl 7052 1idpru 7053 recexprlem1ssl 7095 recexprlem1ssu 7096 msqge0 7993 mulge0 7996 divsubdirap 8073 divdiv32ap 8085 peano2uz 8966 fzoshftral 9538 expdivap 9843 ibcval5 10006 redivap 10135 imdivap 10142 absdiflt 10352 absdifle 10353 lcmgcdeq 10845 isprm3 10880 prmdvdsexpb 10908 |
Copyright terms: Public domain | W3C validator |