| 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 1129 | . 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 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: syl312anc 1393 syl321anc 1394 syl313anc 1396 syl331anc 1397 fprlem1 8325 pythagtrip 16872 nmolb2d 24739 nmoleub 24752 clwwisshclwwslem 30033 numclwwlk1lem2foa 30373 cvlcvr1 39340 4atlem12b 39613 dalawlem10 39882 dalawlem13 39885 dalawlem15 39887 osumcllem11N 39968 lhp2atne 40036 lhp2at0ne 40038 cdlemd 40209 ltrneq3 40210 cdleme7d 40248 cdlemeg49le 40513 cdleme 40562 cdlemg1a 40572 ltrniotavalbN 40586 cdlemg44 40735 cdlemk19 40871 cdlemk27-3 40909 cdlemk33N 40911 cdlemk34 40912 cdlemk49 40953 cdlemk53a 40957 cdlemk19u 40972 cdlemk56w 40975 dia2dimlem4 41069 dih1dimatlem0 41330 itsclc0yqe 48682 itsclinecirc0 48694 itsclinecirc0b 48695 inlinecirc02plem 48707 |
| Copyright terms: Public domain | W3C validator |