![]() |
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 10261 modifeq2int 10386 modaddmodup 10387 seq3f1olemqsum 10500 seq3f1o 10504 exple1 10576 leexp2rd 10684 nn0ltexp2 10689 facubnd 10725 permnn 10751 dfabsmax 11226 expcnvre 11511 dvdsadd2b 11847 dvdsmulgcd 12026 sqgcd 12030 bezoutr 12033 cncongr2 12104 pw2dvds 12166 hashgcdlem 12238 modprm0 12254 modprmn0modprm0 12256 tgioo 14049 lgssq 14444 lgssq2 14445 |
Copyright terms: Public domain | W3C validator |