| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > syl312anc | Structured version Visualization version GIF version | ||
| Description: Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.) |
| Ref | Expression |
|---|---|
| syl3anc.1 | ⊢ (𝜑 → 𝜓) |
| syl3anc.2 | ⊢ (𝜑 → 𝜒) |
| syl3anc.3 | ⊢ (𝜑 → 𝜃) |
| syl3Xanc.4 | ⊢ (𝜑 → 𝜏) |
| syl23anc.5 | ⊢ (𝜑 → 𝜂) |
| syl33anc.6 | ⊢ (𝜑 → 𝜁) |
| syl312anc.7 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁)) → 𝜎) |
| Ref | Expression |
|---|---|
| syl312anc | ⊢ (𝜑 → 𝜎) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syl3anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
| 2 | syl3anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
| 3 | syl3anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
| 4 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
| 5 | syl23anc.5 | . . 3 ⊢ (𝜑 → 𝜂) | |
| 6 | syl33anc.6 | . . 3 ⊢ (𝜑 → 𝜁) | |
| 7 | 5, 6 | jca 511 | . 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁)) |
| 8 | syl312anc.7 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁)) → 𝜎) | |
| 9 | 1, 2, 3, 4, 7, 8 | syl311anc 1386 | 1 ⊢ (𝜑 → 𝜎) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ 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: pythagtriplem19 16871 cdleme27cl 40368 cdlemefs27cl 40415 cdleme32fvcl 40442 cdlemg16ALTN 40660 cdlemg27a 40694 cdlemg31c 40701 cdlemg39 40718 cdlemk11ta 40931 cdlemk19ylem 40932 cdlemk11tc 40947 cdlemk45 40949 dihmeetlem12N 41320 dihjatc 41419 flt4lem5c 42664 flt4lem5d 42665 flt4lem5e 42666 |
| Copyright terms: Public domain | W3C validator |