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 1167 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
3 | syl3an1.2 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | syl 14 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 962 |
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 964 |
This theorem is referenced by: syl3an1b 1252 syl3an1br 1255 wepo 4281 f1ofveu 5762 fovrnda 5914 smoiso 6199 tfrcl 6261 omv 6351 oeiv 6352 nndi 6382 nnmsucr 6384 f1oen2g 6649 f1dom2g 6650 undiffi 6813 prarloclemarch2 7227 distrnq0 7267 ltprordil 7397 1idprl 7398 1idpru 7399 ltpopr 7403 ltexprlemopu 7411 ltexprlemdisj 7414 ltexprlemfl 7417 ltexprlemfu 7419 ltexprlemru 7420 recexprlemdisj 7438 recexprlemss1l 7443 recexprlemss1u 7444 cnegexlem1 7937 msqge0 8378 mulge0 8381 divnegap 8466 divdiv32ap 8480 divneg2ap 8496 peano2uz 9378 lbzbi 9408 negqmod0 10104 modqmuladdnn0 10141 expnlbnd 10416 shftfvalg 10590 xrmaxaddlem 11029 retanclap 11429 tannegap 11435 demoivreALT 11480 gcd0id 11667 isprm3 11799 euclemma 11824 phiprmpw 11898 psmetcl 12495 xmetcl 12521 metcl 12522 meteq0 12529 metge0 12535 metsym 12540 blelrnps 12588 blelrn 12589 blssm 12590 blres 12603 mscl 12634 xmscl 12635 xmsge0 12636 xmseq0 12637 xmssym 12638 mopnin 12656 sincosq1sgn 12907 sincosq2sgn 12908 sincosq3sgn 12909 sincosq4sgn 12910 |
Copyright terms: Public domain | W3C validator |