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 553 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
4 | syl12anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
5 | syl22anc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl23anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) | |
8 | 3, 4, 5, 6, 7 | syl13anc 1320 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: suppofss1d 7219 suppofss2d 7220 cnfcomlem 8479 ackbij1lem16 8940 div2subd 10730 symg2bas 17641 evl1expd 19530 psgndiflemA 19766 oftpos 20077 restopn2 20791 tsmsxp 21768 blcld 22120 metustexhalf 22171 cnllycmp 22563 dvlipcn 23561 tanregt0 24089 ostthlem1 25116 ax5seglem6 25614 axcontlem4 25647 axcontlem7 25650 wwlkextwrd 26256 pnfneige0 29325 qqhval2 29354 esumcocn 29469 carsgmon 29703 bnj1125 30314 heiborlem8 32787 2atjm 33749 1cvrat 33780 lvolnlelln 33888 lvolnlelpln 33889 4atlem3 33900 lplncvrlvol 33920 dalem39 34015 cdleme4a 34544 cdleme15 34583 cdleme16c 34585 cdleme19b 34610 cdleme19e 34613 cdleme20d 34618 cdleme20g 34621 cdleme20j 34624 cdleme20k 34625 cdleme20l2 34627 cdleme20l 34628 cdleme20m 34629 cdleme22e 34650 cdleme22eALTN 34651 cdleme22f 34652 cdleme27cl 34672 cdlemefr27cl 34709 mpaaeu 36739 wwlksnextwrd 41103 |
Copyright terms: Public domain | W3C validator |