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 1127 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
5 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl311anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁) | |
8 | 4, 5, 6, 7 | syl3anc 1370 | 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 206 df-an 397 df-3an 1088 |
This theorem is referenced by: syl312anc 1390 syl321anc 1391 syl313anc 1393 syl331anc 1394 fprlem1 8107 pythagtrip 16533 nmolb2d 23880 nmoleub 23893 clwwisshclwwslem 28374 numclwwlk1lem2foa 28714 cvlcvr1 37349 4atlem12b 37621 dalawlem10 37890 dalawlem13 37893 dalawlem15 37895 osumcllem11N 37976 lhp2atne 38044 lhp2at0ne 38046 cdlemd 38217 ltrneq3 38218 cdleme7d 38256 cdlemeg49le 38521 cdleme 38570 cdlemg1a 38580 ltrniotavalbN 38594 cdlemg44 38743 cdlemk19 38879 cdlemk27-3 38917 cdlemk33N 38919 cdlemk34 38920 cdlemk49 38961 cdlemk53a 38965 cdlemk19u 38980 cdlemk56w 38983 dia2dimlem4 39077 dih1dimatlem0 39338 itsclc0yqe 46076 itsclinecirc0 46088 itsclinecirc0b 46089 inlinecirc02plem 46101 |
Copyright terms: Public domain | W3C validator |