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 966 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | |
2 | simp2 967 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | |
3 | syld3an3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
4 | syld3an3.2 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) | |
5 | 1, 2, 3, 4 | syl3anc 1201 | 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: syld3an1 1247 syld3an2 1248 brelrng 4740 moriotass 5726 nnncan1 7966 lediv1 8595 modqval 10065 modqvalr 10066 modqcl 10067 flqpmodeq 10068 modq0 10070 modqge0 10073 modqlt 10074 modqdiffl 10076 modqdifz 10077 modqvalp1 10084 exp3val 10263 bcval4 10466 dvdsmultr1 11458 dvdssub2 11462 divalglemeuneg 11547 ndvdsadd 11555 basgen2 12177 opnneiss 12254 cnpf2 12303 sincosq1lem 12833 |
Copyright terms: Public domain | W3C validator |