![]() |
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 964 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | simp2 965 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | |
3 | syld3an3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
4 | syld3an3.2 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) | |
5 | 1, 2, 3, 4 | syl3anc 1199 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 945 |
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 947 |
This theorem is referenced by: syld3an1 1245 syld3an2 1246 brelrng 4730 moriotass 5712 nnncan1 7921 lediv1 8537 modqval 9990 modqvalr 9991 modqcl 9992 flqpmodeq 9993 modq0 9995 modqge0 9998 modqlt 9999 modqdiffl 10001 modqdifz 10002 modqvalp1 10009 exp3val 10188 bcval4 10391 dvdsmultr1 11379 dvdssub2 11383 divalglemeuneg 11468 ndvdsadd 11476 basgen2 12093 opnneiss 12170 cnpf2 12218 |
Copyright terms: Public domain | W3C validator |