![]() |
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 1168 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
3 | syl3an1.2 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | syl 14 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 963 |
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 965 |
This theorem is referenced by: syl3an1b 1253 syl3an1br 1256 wepo 4289 f1ofveu 5770 fovrnda 5922 smoiso 6207 tfrcl 6269 omv 6359 oeiv 6360 nndi 6390 nnmsucr 6392 f1oen2g 6657 f1dom2g 6658 undiffi 6821 prarloclemarch2 7251 distrnq0 7291 ltprordil 7421 1idprl 7422 1idpru 7423 ltpopr 7427 ltexprlemopu 7435 ltexprlemdisj 7438 ltexprlemfl 7441 ltexprlemfu 7443 ltexprlemru 7444 recexprlemdisj 7462 recexprlemss1l 7467 recexprlemss1u 7468 cnegexlem1 7961 msqge0 8402 mulge0 8405 divnegap 8490 divdiv32ap 8504 divneg2ap 8520 peano2uz 9405 lbzbi 9435 negqmod0 10135 modqmuladdnn0 10172 expnlbnd 10447 shftfvalg 10622 xrmaxaddlem 11061 retanclap 11465 tannegap 11471 demoivreALT 11516 gcd0id 11703 isprm3 11835 euclemma 11860 phiprmpw 11934 psmetcl 12534 xmetcl 12560 metcl 12561 meteq0 12568 metge0 12574 metsym 12579 blelrnps 12627 blelrn 12628 blssm 12629 blres 12642 mscl 12673 xmscl 12674 xmsge0 12675 xmseq0 12676 xmssym 12677 mopnin 12695 sincosq1sgn 12955 sincosq2sgn 12956 sincosq3sgn 12957 sincosq4sgn 12958 |
Copyright terms: Public domain | W3C validator |