![]() |
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 513 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
4 | syl3anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
5 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl211anc.5 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂) | |
7 | 3, 4, 5, 6 | syl3anc 1372 | 1 ⊢ (𝜑 → 𝜂) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 |
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 206 df-an 398 df-3an 1090 |
This theorem is referenced by: syl212anc 1381 syl221anc 1382 frrlem15 9747 supicc 13473 modaddmulmod 13898 limsupgre 15420 limsupbnd1 15421 limsupbnd2 15422 lbspss 20680 lindff1 21358 islinds4 21373 mdetunilem9 22103 madutpos 22125 neiptopnei 22617 mbflimsup 25164 cxpneg 26170 cxpmul2 26178 cxpsqrt 26192 cxpaddd 26206 cxpsubd 26207 divcxpd 26211 fsumharmonic 26495 bposlem1 26766 lgsqr 26833 chpchtlim 26961 sltmul2d 27603 ax5seg 28175 archiabllem2c 32318 qsidomlem2 32529 logdivsqrle 33599 lindsadd 36418 lshpnelb 37791 cdlemg2fv2 39408 cdlemg2m 39412 cdlemg9a 39440 cdlemg9b 39441 cdlemg12b 39452 cdlemg14f 39461 cdlemg14g 39462 cdlemg17dN 39471 cdlemkj 39671 cdlemkuv2 39675 cdlemk52 39762 cdlemk53a 39763 mullimc 44266 mullimcf 44273 sfprmdvdsmersenne 46205 lincfsuppcl 46995 |
Copyright terms: Public domain | W3C validator |