![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl23anc | Structured version Visualization version GIF version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
syl12anc.1 | ⊢ (𝜑 → 𝜓) |
syl12anc.2 | ⊢ (𝜑 → 𝜒) |
syl12anc.3 | ⊢ (𝜑 → 𝜃) |
syl22anc.4 | ⊢ (𝜑 → 𝜏) |
syl23anc.5 | ⊢ (𝜑 → 𝜂) |
syl23anc.6 | ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) |
Ref | Expression |
---|---|
syl23anc | ⊢ (𝜑 → 𝜁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl12anc.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | syl12anc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | 1, 2 | jca 501 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
4 | syl12anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
5 | syl22anc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl23anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) | |
8 | 3, 4, 5, 6, 7 | syl13anc 1478 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 ∧ w3a 1071 |
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 197 df-an 383 df-3an 1073 |
This theorem is referenced by: suppofss1d 7487 suppofss2d 7488 cnfcomlem 8763 ackbij1lem16 9262 div2subd 11056 symg2bas 18024 evl1expd 19923 psgndiflemA 20162 oftpos 20475 restopn2 21201 tsmsxp 22177 blcld 22529 metustexhalf 22580 cnllycmp 22974 dvlipcn 23976 tanregt0 24505 ostthlem1 25536 ax5seglem6 26034 axcontlem4 26067 axcontlem7 26070 wwlksnextwrd 27040 pnfneige0 30336 qqhval2 30365 esumcocn 30481 carsgmon 30715 bnj1125 31397 nosupbnd1lem1 32190 nosupbnd2 32198 heiborlem8 33948 2atjm 35253 1cvrat 35284 lvolnlelln 35392 lvolnlelpln 35393 4atlem3 35404 lplncvrlvol 35424 dalem39 35519 cdleme4a 36048 cdleme15 36087 cdleme16c 36089 cdleme19b 36113 cdleme19e 36116 cdleme20d 36121 cdleme20g 36124 cdleme20j 36127 cdleme20k 36128 cdleme20l2 36130 cdleme20l 36131 cdleme20m 36132 cdleme22e 36153 cdleme22eALTN 36154 cdleme22f 36155 cdleme27cl 36175 cdlemefr27cl 36212 mpaaeu 38246 |
Copyright terms: Public domain | W3C validator |