![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl32anc | GIF version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 | ⊢ (𝜑 → 𝜓) |
sylXanc.2 | ⊢ (𝜑 → 𝜒) |
sylXanc.3 | ⊢ (𝜑 → 𝜃) |
sylXanc.4 | ⊢ (𝜑 → 𝜏) |
sylXanc.5 | ⊢ (𝜑 → 𝜂) |
syl32anc.6 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁) |
Ref | Expression |
---|---|
syl32anc | ⊢ (𝜑 → 𝜁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | sylXanc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | sylXanc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
4 | sylXanc.4 | . . 3 ⊢ (𝜑 → 𝜏) | |
5 | sylXanc.5 | . . 3 ⊢ (𝜑 → 𝜂) | |
6 | 4, 5 | jca 306 | . 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂)) |
7 | syl32anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁) | |
8 | 1, 2, 3, 6, 7 | syl31anc 1241 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 978 |
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 980 |
This theorem is referenced by: ioom 10263 modifeq2int 10388 modaddmodup 10389 seq3f1olemqsum 10502 seq3f1o 10506 exple1 10578 leexp2rd 10686 nn0ltexp2 10691 facubnd 10727 permnn 10753 dfabsmax 11228 expcnvre 11513 dvdsadd2b 11849 dvdsmulgcd 12028 sqgcd 12032 bezoutr 12035 cncongr2 12106 pw2dvds 12168 hashgcdlem 12240 modprm0 12256 modprmn0modprm0 12258 tgioo 14131 lgssq 14526 lgssq2 14527 |
Copyright terms: Public domain | W3C validator |