| 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 511 | . 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 395 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: syl212anc 1382 syl221anc 1383 frrlem15 9797 supicc 13541 modaddmulmod 13979 limsupgre 15517 limsupbnd1 15518 limsupbnd2 15519 lbspss 21081 lindff1 21840 islinds4 21855 mdetunilem9 22626 madutpos 22648 neiptopnei 23140 mbflimsup 25701 cxpneg 26723 cxpmul2 26731 cxpsqrt 26745 cxpaddd 26759 cxpsubd 26760 divcxpd 26764 fsumharmonic 27055 bposlem1 27328 lgsqr 27395 chpchtlim 27523 sltmul2d 28198 ax5seg 28953 archiabllem2c 33202 qsidomlem2 33481 dimlssid 33683 logdivsqrle 34665 lindsadd 37620 lshpnelb 38985 cdlemg2fv2 40602 cdlemg2m 40606 cdlemg9a 40634 cdlemg9b 40635 cdlemg12b 40646 cdlemg14f 40655 cdlemg14g 40656 cdlemg17dN 40665 cdlemkj 40865 cdlemkuv2 40869 cdlemk52 40956 cdlemk53a 40957 mullimc 45631 mullimcf 45638 sfprmdvdsmersenne 47590 lincfsuppcl 48330 |
| Copyright terms: Public domain | W3C validator |