![]() |
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 999 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | simp2 1000 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | |
3 | syld3an3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
4 | syld3an3.2 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) | |
5 | 1, 2, 3, 4 | syl3anc 1249 | 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: syld3an1 1295 syld3an2 1296 brelrng 4879 moriotass 5884 nnncan1 8228 lediv1 8861 modqval 10361 modqvalr 10362 modqcl 10363 flqpmodeq 10364 modq0 10366 modqge0 10369 modqlt 10370 modqdiffl 10372 modqdifz 10373 modqvalp1 10380 exp3val 10562 bcval4 10773 dvdsmultr1 11879 dvdssub2 11883 divalglemeuneg 11969 ndvdsadd 11977 grpsubf 13046 grpinvsub 13049 grpnpcan 13059 mulginvcom 13112 mulginvinv 13113 subgsubcl 13149 qussub 13201 ghmsub 13215 dvrcl 13510 unitdvcl 13511 basgen2 14066 opnneiss 14143 cnpf2 14192 sincosq1lem 14731 |
Copyright terms: Public domain | W3C validator |