![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl31anc | GIF version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 | ⊢ (𝜑 → 𝜓) |
sylXanc.2 | ⊢ (𝜑 → 𝜒) |
sylXanc.3 | ⊢ (𝜑 → 𝜃) |
sylXanc.4 | ⊢ (𝜑 → 𝜏) |
syl31anc.5 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) |
Ref | Expression |
---|---|
syl31anc | ⊢ (𝜑 → 𝜂) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | sylXanc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | sylXanc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | 1, 2, 3 | 3jca 1129 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
5 | sylXanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl31anc.5 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) | |
7 | 4, 5, 6 | syl2anc 406 | 1 ⊢ (𝜑 → 𝜂) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 930 |
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 932 |
This theorem is referenced by: syl32anc 1192 stoic4b 1377 enq0tr 7143 ltmul12a 8476 lt2msq1 8501 ledivp1 8519 lemul1ad 8555 lemul2ad 8556 lediv2ad 9353 xaddge0 9502 difelfznle 9753 expubnd 10191 expcanlem 10303 expcand 10305 xrmaxaddlem 10868 mertenslemi1 11143 eftlub 11194 dvdsadd 11331 divalgmod 11419 gcdzeq 11503 rplpwr 11508 sqgcd 11510 bezoutr 11513 rpmulgcd2 11569 rpdvds 11573 divgcdodd 11614 oddpwdclemxy 11639 divnumden 11666 crth 11692 phimullem 11693 xblss2ps 12332 xblss2 12333 metcnpi3 12441 limcimolemlt 12513 |
Copyright terms: Public domain | W3C validator |