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 553 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
4 | syl12anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
5 | syl22anc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl211anc.5 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂) | |
7 | 3, 4, 5, 6 | syl3anc 1318 | 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: syl212anc 1328 syl221anc 1329 supicc 12191 modaddmulmod 12599 limsupgre 14060 limsupbnd1 14061 limsupbnd2 14062 lbspss 18903 lindff1 19978 islinds4 19993 mdetunilem9 20245 madutpos 20267 neiptopnei 20746 mbflimsup 23239 cxpneg 24227 cxpmul2 24235 cxpsqrt 24249 cxpaddd 24263 cxpsubd 24264 divcxpd 24268 fsumharmonic 24538 bposlem1 24809 lgsqr 24876 chpchtlim 24968 ax5seg 25618 archiabllem2c 29080 lshpnelb 33289 cdlemg2fv2 34906 cdlemg2m 34910 cdlemg9a 34938 cdlemg9b 34939 cdlemg12b 34950 cdlemg14f 34959 cdlemg14g 34960 cdlemg17dN 34969 cdlemkj 35169 cdlemkuv2 35173 cdlemk52 35260 cdlemk53a 35261 mullimc 38683 mullimcf 38690 sfprmdvdsmersenne 40058 lincfsuppcl 41996 |
Copyright terms: Public domain | W3C validator |