![]() |
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 507 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
4 | syl3anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
5 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl23anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) | |
8 | 3, 4, 5, 6, 7 | syl13anc 1440 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ 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 199 df-an 387 df-3an 1073 |
This theorem is referenced by: suppofss1d 7616 suppofss2d 7617 cnfcomlem 8895 ackbij1lem16 9394 div2subd 11203 symg2bas 18205 evl1expd 20109 psgndiflemA 20347 oftpos 20667 restopn2 21393 tsmsxp 22370 blcld 22722 metustexhalf 22773 cnllycmp 23167 dvlipcn 24198 tanregt0 24727 ostthlem1 25772 ax5seglem6 26287 axcontlem4 26320 axcontlem7 26323 wwlksnextwrd 27265 wwlksnextwrdOLD 27270 lindsunlem 30442 pnfneige0 30599 qqhval2 30628 esumcocn 30744 carsgmon 30978 bnj1125 31663 nosupbnd1lem1 32447 nosupbnd2 32455 heiborlem8 34246 2atjm 35604 1cvrat 35635 lvolnlelln 35743 lvolnlelpln 35744 4atlem3 35755 lplncvrlvol 35775 dalem39 35870 cdleme4a 36398 cdleme15 36437 cdleme16c 36439 cdleme19b 36463 cdleme19e 36466 cdleme20d 36471 cdleme20g 36474 cdleme20j 36477 cdleme20k 36478 cdleme20l2 36480 cdleme20l 36481 cdleme20m 36482 cdleme22e 36503 cdleme22eALTN 36504 cdleme22f 36505 cdleme27cl 36525 cdlemefr27cl 36562 mpaaeu 38689 |
Copyright terms: Public domain | W3C validator |