![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl13anc | GIF version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 | ⊢ (𝜑 → 𝜓) |
sylXanc.2 | ⊢ (𝜑 → 𝜒) |
sylXanc.3 | ⊢ (𝜑 → 𝜃) |
sylXanc.4 | ⊢ (𝜑 → 𝜏) |
syl13anc.5 | ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂) |
Ref | Expression |
---|---|
syl13anc | ⊢ (𝜑 → 𝜂) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | sylXanc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | sylXanc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | sylXanc.4 | . . 3 ⊢ (𝜑 → 𝜏) | |
5 | 2, 3, 4 | 3jca 1121 | . 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏)) |
6 | syl13anc.5 | . 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂) | |
7 | 1, 5, 6 | syl2anc 403 | 1 ⊢ (𝜑 → 𝜂) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 922 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 924 |
This theorem is referenced by: syl23anc 1179 syl33anc 1187 caovassd 5742 caovcand 5745 caovordid 5749 caovordd 5751 caovdid 5758 caovdird 5761 swoer 6253 swoord1 6254 swoord2 6255 suplub2ti 6617 prarloclem3 6977 fzosubel3 9510 iseqsplit 9787 iseqcaopr 9791 divalglemex 10716 |
Copyright terms: Public domain | W3C validator |