![]() |
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 1187 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
3 | syl3an1.2 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | syl 14 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 980 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: syl3an1b 1285 syl3an1br 1288 wepo 4374 f1ofveu 5880 fovcdmda 6036 smoiso 6322 tfrcl 6384 omv 6475 oeiv 6476 nndi 6506 nnmsucr 6508 f1oen2g 6776 f1dom2g 6777 undiffi 6948 prarloclemarch2 7443 distrnq0 7483 ltprordil 7613 1idprl 7614 1idpru 7615 ltpopr 7619 ltexprlemopu 7627 ltexprlemdisj 7630 ltexprlemfl 7633 ltexprlemfu 7635 ltexprlemru 7636 recexprlemdisj 7654 recexprlemss1l 7659 recexprlemss1u 7660 cnegexlem1 8157 msqge0 8598 mulge0 8601 divnegap 8688 divdiv32ap 8702 divneg2ap 8718 peano2uz 9608 lbzbi 9641 negqmod0 10357 modqmuladdnn0 10394 expnlbnd 10671 shftfvalg 10854 xrmaxaddlem 11295 retanclap 11757 tannegap 11763 demoivreALT 11808 gcd0id 12007 isprm3 12145 euclemma 12173 phiprmpw 12249 fermltl 12261 sgrpcl 12865 mndcl 12877 grpcl 12946 dfgrp2 12964 grprcan 12974 grpsubcl 13017 imasgrp2 13045 mhmid 13050 mhmmnd 13051 mulginvcom 13080 mulgnndir 13084 mulgnnass 13090 qusgrp 13164 ghmmulg 13188 ghmrn 13189 ghmeqker 13203 ablcom 13235 ablinvadd 13242 ghmcmn 13258 rngacl 13289 rngpropd 13302 srgacl 13329 srgcom 13330 ringacl 13377 imasring 13407 subrngacl 13548 subrgacl 13572 subrgugrp 13580 lmodacl 13608 lmodmcl 13609 lmodvacl 13611 lmodvsubcl 13641 lmod4 13646 lmodvaddsub4 13648 lmodvpncan 13649 lmodvnpcan 13650 lmodsubeq0 13655 psmetcl 14263 xmetcl 14289 metcl 14290 meteq0 14297 metge0 14303 metsym 14308 blelrnps 14356 blelrn 14357 blssm 14358 blres 14371 mscl 14402 xmscl 14403 xmsge0 14404 xmseq0 14405 xmssym 14406 mopnin 14424 sincosq1sgn 14684 sincosq2sgn 14685 sincosq3sgn 14686 sincosq4sgn 14687 lgsneg1 14864 |
Copyright terms: Public domain | W3C validator |