![]() |
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 1125 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
5 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl311anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁) | |
8 | 4, 5, 6, 7 | syl3anc 1368 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1084 |
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 395 df-3an 1086 |
This theorem is referenced by: syl312anc 1388 syl321anc 1389 syl313anc 1391 syl331anc 1392 fprlem1 8306 pythagtrip 16806 nmolb2d 24679 nmoleub 24692 clwwisshclwwslem 29896 numclwwlk1lem2foa 30236 cvlcvr1 38941 4atlem12b 39214 dalawlem10 39483 dalawlem13 39486 dalawlem15 39488 osumcllem11N 39569 lhp2atne 39637 lhp2at0ne 39639 cdlemd 39810 ltrneq3 39811 cdleme7d 39849 cdlemeg49le 40114 cdleme 40163 cdlemg1a 40173 ltrniotavalbN 40187 cdlemg44 40336 cdlemk19 40472 cdlemk27-3 40510 cdlemk33N 40512 cdlemk34 40513 cdlemk49 40554 cdlemk53a 40558 cdlemk19u 40573 cdlemk56w 40576 dia2dimlem4 40670 dih1dimatlem0 40931 itsclc0yqe 48020 itsclinecirc0 48032 itsclinecirc0b 48033 inlinecirc02plem 48045 |
Copyright terms: Public domain | W3C validator |