![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl3an1 | GIF version |
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
Ref | Expression |
---|---|
syl3an1.1 | ⊢ (𝜑 → 𝜓) |
syl3an1.2 | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
syl3an1 | ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3an1.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | 3anim1i 1125 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
3 | syl3an1.2 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | syl 14 | 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: syl3an1b 1206 syl3an1br 1209 wepo 4122 f1ofveu 5531 fovrnda 5675 smoiso 5951 tfrcl 6013 omv 6099 oeiv 6100 nndi 6130 nnmsucr 6132 f1oen2g 6302 f1dom2g 6303 prarloclemarch2 6671 distrnq0 6711 ltprordil 6841 1idprl 6842 1idpru 6843 ltpopr 6847 ltexprlemopu 6855 ltexprlemdisj 6858 ltexprlemfl 6861 ltexprlemfu 6863 ltexprlemru 6864 recexprlemdisj 6882 recexprlemss1l 6887 recexprlemss1u 6888 cnegexlem1 7350 msqge0 7783 mulge0 7786 divnegap 7861 divdiv32ap 7875 divneg2ap 7891 peano2uz 8752 lbzbi 8782 negqmod0 9413 modqmuladdnn0 9450 expnlbnd 9694 shftfvalg 9844 gcd0id 10514 isprm3 10644 euclemma 10669 |
Copyright terms: Public domain | W3C validator |