| 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 |
|---|---|
| syl3anc.1 | ⊢ (𝜑 → 𝜓) |
| syl3anc.2 | ⊢ (𝜑 → 𝜒) |
| syl3anc.3 | ⊢ (𝜑 → 𝜃) |
| syl3Xanc.4 | ⊢ (𝜑 → 𝜏) |
| syl23anc.5 | ⊢ (𝜑 → 𝜂) |
| syl33anc.6 | ⊢ (𝜑 → 𝜁) |
| syl133anc.7 | ⊢ (𝜑 → 𝜎) |
| syl331anc.8 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ 𝜎) → 𝜌) |
| Ref | Expression |
|---|---|
| syl331anc | ⊢ (𝜑 → 𝜌) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syl3anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
| 2 | syl3anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
| 3 | syl3anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
| 4 | syl3Xanc.4 | . . 3 ⊢ (𝜑 → 𝜏) | |
| 5 | syl23anc.5 | . . 3 ⊢ (𝜑 → 𝜂) | |
| 6 | syl33anc.6 | . . 3 ⊢ (𝜑 → 𝜁) | |
| 7 | 4, 5, 6 | 3jca 1129 | . 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂 ∧ 𝜁)) |
| 8 | syl133anc.7 | . 2 ⊢ (𝜑 → 𝜎) | |
| 9 | syl331anc.8 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ 𝜎) → 𝜌) | |
| 10 | 1, 2, 3, 7, 8, 9 | syl311anc 1386 | 1 ⊢ (𝜑 → 𝜌) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: syl332anc 1403 syl333anc 1404 qredeu 16695 brbtwn2 28920 3atlem4 39488 3atlem6 39490 llnexchb2 39871 osumcllem9N 39966 cdlemd4 40203 cdleme26fALTN 40364 cdleme26f 40365 cdleme36m 40463 cdlemg17b 40664 cdlemg17h 40670 cdlemk38 40917 cdlemk53b 40958 cdlemkyyN 40964 cdlemk43N 40965 |
| Copyright terms: Public domain | W3C validator |