| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > syl311anc | 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 | ⊢ (𝜑 → 𝜂) |
| syl311anc.6 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁) |
| Ref | Expression |
|---|---|
| syl311anc | ⊢ (𝜑 → 𝜁) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syl3anc.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
| 2 | syl3anc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
| 3 | syl3anc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
| 4 | 1, 2, 3 | 3jca 1128 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
| 5 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
| 6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
| 7 | syl311anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁) | |
| 8 | 4, 5, 6, 7 | syl3anc 1373 | 1 ⊢ (𝜑 → 𝜁) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1086 |
| 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 1088 |
| This theorem is referenced by: syl312anc 1393 syl321anc 1394 syl313anc 1396 syl331anc 1397 fprlem1 8281 pythagtrip 16811 nmolb2d 24612 nmoleub 24625 clwwisshclwwslem 29949 numclwwlk1lem2foa 30289 cvlcvr1 39327 4atlem12b 39600 dalawlem10 39869 dalawlem13 39872 dalawlem15 39874 osumcllem11N 39955 lhp2atne 40023 lhp2at0ne 40025 cdlemd 40196 ltrneq3 40197 cdleme7d 40235 cdlemeg49le 40500 cdleme 40549 cdlemg1a 40559 ltrniotavalbN 40573 cdlemg44 40722 cdlemk19 40858 cdlemk27-3 40896 cdlemk33N 40898 cdlemk34 40899 cdlemk49 40940 cdlemk53a 40944 cdlemk19u 40959 cdlemk56w 40962 dia2dimlem4 41056 dih1dimatlem0 41317 itsclc0yqe 48740 itsclinecirc0 48752 itsclinecirc0b 48753 inlinecirc02plem 48765 |
| Copyright terms: Public domain | W3C validator |