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 |
---|---|
syl3anc.1 | ⊢ (𝜑 → 𝜓) |
syl3anc.2 | ⊢ (𝜑 → 𝜒) |
syl3anc.3 | ⊢ (𝜑 → 𝜃) |
syl3Xanc.4 | ⊢ (𝜑 → 𝜏) |
syl211anc.5 | ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂) |
Ref | Expression |
---|---|
syl211anc | ⊢ (𝜑 → 𝜂) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3anc.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | syl3anc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | 1, 2 | jca 515 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
4 | syl3anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
5 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl211anc.5 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂) | |
7 | 3, 4, 5, 6 | syl3anc 1373 | 1 ⊢ (𝜑 → 𝜂) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: syl212anc 1382 syl221anc 1383 frrlem15 9373 supicc 13089 modaddmulmod 13511 limsupgre 15042 limsupbnd1 15043 limsupbnd2 15044 lbspss 20119 lindff1 20782 islinds4 20797 mdetunilem9 21517 madutpos 21539 neiptopnei 22029 mbflimsup 24563 cxpneg 25569 cxpmul2 25577 cxpsqrt 25591 cxpaddd 25605 cxpsubd 25606 divcxpd 25610 fsumharmonic 25894 bposlem1 26165 lgsqr 26232 chpchtlim 26360 ax5seg 27029 archiabllem2c 31168 qsidomlem2 31343 logdivsqrle 32342 lindsadd 35507 lshpnelb 36735 cdlemg2fv2 38351 cdlemg2m 38355 cdlemg9a 38383 cdlemg9b 38384 cdlemg12b 38395 cdlemg14f 38404 cdlemg14g 38405 cdlemg17dN 38414 cdlemkj 38614 cdlemkuv2 38618 cdlemk52 38705 cdlemk53a 38706 mullimc 42832 mullimcf 42839 sfprmdvdsmersenne 44728 lincfsuppcl 45427 |
Copyright terms: Public domain | W3C validator |