Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syl332anc | 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 | ⊢ (𝜑 → 𝜂) |
syl33anc.6 | ⊢ (𝜑 → 𝜁) |
syl133anc.7 | ⊢ (𝜑 → 𝜎) |
syl233anc.8 | ⊢ (𝜑 → 𝜌) |
syl332anc.9 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇) |
Ref | Expression |
---|---|
syl332anc | ⊢ (𝜑 → 𝜇) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl3anc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | syl3anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
4 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
5 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
6 | syl33anc.6 | . 2 ⊢ (𝜑 → 𝜁) | |
7 | syl133anc.7 | . . 3 ⊢ (𝜑 → 𝜎) | |
8 | syl233anc.8 | . . 3 ⊢ (𝜑 → 𝜌) | |
9 | 7, 8 | jca 514 | . 2 ⊢ (𝜑 → (𝜎 ∧ 𝜌)) |
10 | syl332anc.9 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇) | |
11 | 1, 2, 3, 4, 5, 6, 9, 10 | syl331anc 1391 | 1 ⊢ (𝜑 → 𝜇) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 |
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 209 df-an 399 df-3an 1085 |
This theorem is referenced by: mdetunilem5 21224 mdetuni0 21229 lnjatN 36915 lncmp 36918 cdlema1N 36926 4atexlemex6 37209 cdlemd4 37336 cdleme18c 37428 cdleme18d 37430 cdleme19b 37439 cdleme21ct 37464 cdleme21d 37465 cdleme21e 37466 cdleme21k 37473 cdleme22g 37483 cdleme24 37487 cdleme27a 37502 cdleme27N 37504 cdleme28a 37505 cdleme40n 37603 cdlemg16zz 37795 cdlemg37 37824 cdlemk21-2N 38026 cdlemk20-2N 38027 cdlemk28-3 38043 cdlemk19xlem 38077 |
Copyright terms: Public domain | W3C validator |