| 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 |
|---|---|
| syl3anc.1 | ⊢ (𝜑 → 𝜓) |
| syl3anc.2 | ⊢ (𝜑 → 𝜒) |
| syl3anc.3 | ⊢ (𝜑 → 𝜃) |
| syl3Xanc.4 | ⊢ (𝜑 → 𝜏) |
| syl23anc.5 | ⊢ (𝜑 → 𝜂) |
| syl23anc.6 | ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) |
| Ref | Expression |
|---|---|
| syl23anc | ⊢ (𝜑 → 𝜁) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syl3anc.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
| 2 | syl3anc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
| 3 | 1, 2 | jca 511 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
| 4 | syl3anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
| 5 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
| 6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
| 7 | syl23anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) | |
| 8 | 3, 4, 5, 6, 7 | syl13anc 1374 | 1 ⊢ (𝜑 → 𝜁) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ 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: suppofss1d 8229 suppofss2d 8230 cnfcomlem 9739 ackbij1lem16 10274 div2subd 12093 symg2bas 19410 psgndiflemA 21619 evl1expd 22349 evls1maplmhm 22381 oftpos 22458 restopn2 23185 tsmsxp 24163 blcld 24518 cnllycmp 24988 dvlipcn 26033 tanregt0 26581 ostthlem1 27671 nosupbnd1lem1 27753 nosupbnd2 27761 noinfbnd1lem1 27768 noinfbnd2 27776 ax5seglem6 28949 axcontlem4 28982 axcontlem7 28985 wwlksnextwrd 29917 drngidlhash 33462 rhmpreimaprmidl 33479 qsdrngilem 33522 rsprprmprmidlb 33551 rprmirredb 33560 dfufd2lem 33577 lindsunlem 33675 lactlmhm 33685 pnfneige0 33950 qqhval2 33983 esumcocn 34081 carsgmon 34316 bnj1125 35006 heiborlem8 37825 2atjm 39447 1cvrat 39478 lvolnlelln 39586 lvolnlelpln 39587 4atlem3 39598 lplncvrlvol 39618 dalem39 39713 cdleme4a 40241 cdleme15 40280 cdleme16c 40282 cdleme19b 40306 cdleme19e 40309 cdleme20d 40314 cdleme20g 40317 cdleme20j 40320 cdleme20k 40321 cdleme20l2 40323 cdleme20l 40324 cdleme20m 40325 cdleme22e 40346 cdleme22eALTN 40347 cdleme22f 40348 cdleme27cl 40368 cdlemefr27cl 40405 mpaaeu 43162 |
| Copyright terms: Public domain | W3C validator |