![]() |
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 1132 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
3 | syl3an1.2 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | syl 14 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 927 |
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 929 |
This theorem is referenced by: syl3an1b 1217 syl3an1br 1220 wepo 4210 f1ofveu 5678 fovrnda 5826 smoiso 6105 tfrcl 6167 omv 6256 oeiv 6257 nndi 6287 nnmsucr 6289 f1oen2g 6552 f1dom2g 6553 undiffi 6715 prarloclemarch2 7075 distrnq0 7115 ltprordil 7245 1idprl 7246 1idpru 7247 ltpopr 7251 ltexprlemopu 7259 ltexprlemdisj 7262 ltexprlemfl 7265 ltexprlemfu 7267 ltexprlemru 7268 recexprlemdisj 7286 recexprlemss1l 7291 recexprlemss1u 7292 cnegexlem1 7754 msqge0 8190 mulge0 8193 divnegap 8270 divdiv32ap 8284 divneg2ap 8300 peano2uz 9170 lbzbi 9200 negqmod0 9887 modqmuladdnn0 9924 expnlbnd 10209 shftfvalg 10383 xrmaxaddlem 10819 retanclap 11177 tannegap 11183 demoivreALT 11227 gcd0id 11412 isprm3 11542 euclemma 11567 phiprmpw 11640 psmetcl 12127 xmetcl 12153 metcl 12154 meteq0 12161 metge0 12167 metsym 12172 blelrnps 12220 blelrn 12221 blssm 12222 blres 12235 mscl 12266 xmscl 12267 xmsge0 12268 xmseq0 12269 xmssym 12270 mopnin 12288 |
Copyright terms: Public domain | W3C validator |