Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syl331anc | Structured version Visualization version GIF version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
syl12anc.1 | ⊢ (𝜑 → 𝜓) |
syl12anc.2 | ⊢ (𝜑 → 𝜒) |
syl12anc.3 | ⊢ (𝜑 → 𝜃) |
syl22anc.4 | ⊢ (𝜑 → 𝜏) |
syl23anc.5 | ⊢ (𝜑 → 𝜂) |
syl33anc.6 | ⊢ (𝜑 → 𝜁) |
syl133anc.7 | ⊢ (𝜑 → 𝜎) |
syl331anc.8 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ 𝜎) → 𝜌) |
Ref | Expression |
---|---|
syl331anc | ⊢ (𝜑 → 𝜌) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl12anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl12anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | syl12anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
4 | syl22anc.4 | . . 3 ⊢ (𝜑 → 𝜏) | |
5 | syl23anc.5 | . . 3 ⊢ (𝜑 → 𝜂) | |
6 | syl33anc.6 | . . 3 ⊢ (𝜑 → 𝜁) | |
7 | 4, 5, 6 | 3jca 1235 | . 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂 ∧ 𝜁)) |
8 | syl133anc.7 | . 2 ⊢ (𝜑 → 𝜎) | |
9 | syl331anc.8 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ 𝜎) → 𝜌) | |
10 | 1, 2, 3, 7, 8, 9 | syl311anc 1332 | 1 ⊢ (𝜑 → 𝜌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1031 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 196 df-an 385 df-3an 1033 |
This theorem is referenced by: syl332anc 1349 syl333anc 1350 qredeu 15210 brbtwn2 25585 3atlem4 33790 3atlem6 33792 llnexchb2 34173 osumcllem9N 34268 cdlemd4 34506 cdleme26fALTN 34668 cdleme26f 34669 cdleme36m 34767 cdlemg17b 34968 cdlemg17h 34974 cdlemk38 35221 cdlemk53b 35262 cdlemkyyN 35268 cdlemk43N 35269 |
Copyright terms: Public domain | W3C validator |