Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syld3an3 | GIF version |
Description: A syllogism inference. (Contributed by NM, 20-May-2007.) |
Ref | Expression |
---|---|
syld3an3.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
syld3an3.2 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
syld3an3 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 938 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | simp2 939 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | |
3 | syld3an3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
4 | syld3an3.2 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) | |
5 | 1, 2, 3, 4 | syl3anc 1169 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 919 |
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 921 |
This theorem is referenced by: syld3an1 1215 syld3an2 1216 brelrng 4583 moriotass 5516 nnncan1 7344 lediv1 7947 modqval 9326 modqvalr 9327 modqcl 9328 flqpmodeq 9329 modq0 9331 modqge0 9334 modqlt 9335 modqdiffl 9337 modqdifz 9338 modqvalp1 9345 expival 9478 bcval4 9679 dvdsmultr1 10233 dvdssub2 10237 divalglemeuneg 10323 ndvdsadd 10331 |
Copyright terms: Public domain | W3C validator |