![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl211anc | 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 | ⊢ (𝜑 → 𝜏) |
syl211anc.5 | ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂) |
Ref | Expression |
---|---|
syl211anc | ⊢ (𝜑 → 𝜂) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl12anc.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | syl12anc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | 1, 2 | jca 555 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
4 | syl12anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
5 | syl22anc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl211anc.5 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂) | |
7 | 3, 4, 5, 6 | syl3anc 1407 | 1 ⊢ (𝜑 → 𝜂) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 |
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 385 df-3an 1074 |
This theorem is referenced by: syl212anc 1417 syl221anc 1418 supicc 12402 modaddmulmod 12820 limsupgre 14300 limsupbnd1 14301 limsupbnd2 14302 lbspss 19173 lindff1 20250 islinds4 20265 mdetunilem9 20517 madutpos 20539 neiptopnei 21027 mbflimsup 23521 cxpneg 24515 cxpmul2 24523 cxpsqrt 24537 cxpaddd 24551 cxpsubd 24552 divcxpd 24556 fsumharmonic 24826 bposlem1 25097 lgsqr 25164 chpchtlim 25256 ax5seg 25906 archiabllem2c 29947 logdivsqrle 30926 lshpnelb 34659 cdlemg2fv2 36275 cdlemg2m 36279 cdlemg9a 36307 cdlemg9b 36308 cdlemg12b 36319 cdlemg14f 36328 cdlemg14g 36329 cdlemg17dN 36338 cdlemkj 36538 cdlemkuv2 36542 cdlemk52 36629 cdlemk53a 36630 mullimc 40236 mullimcf 40243 sfprmdvdsmersenne 41915 lincfsuppcl 42597 |
Copyright terms: Public domain | W3C validator |