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 512 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
4 | syl3anc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
5 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl211anc.5 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂) | |
7 | 3, 4, 5, 6 | syl3anc 1363 | 1 ⊢ (𝜑 → 𝜂) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: syl212anc 1372 syl221anc 1373 supicc 12874 modaddmulmod 13294 limsupgre 14826 limsupbnd1 14827 limsupbnd2 14828 lbspss 19783 lindff1 20892 islinds4 20907 mdetunilem9 21157 madutpos 21179 neiptopnei 21668 mbflimsup 24194 cxpneg 25191 cxpmul2 25199 cxpsqrt 25213 cxpaddd 25227 cxpsubd 25228 divcxpd 25232 fsumharmonic 25516 bposlem1 25787 lgsqr 25854 chpchtlim 25982 ax5seg 26651 archiabllem2c 30751 qsidomlem2 30883 logdivsqrle 31820 frrlem15 33039 lindsadd 34766 lshpnelb 36000 cdlemg2fv2 37616 cdlemg2m 37620 cdlemg9a 37648 cdlemg9b 37649 cdlemg12b 37660 cdlemg14f 37669 cdlemg14g 37670 cdlemg17dN 37679 cdlemkj 37879 cdlemkuv2 37883 cdlemk52 37970 cdlemk53a 37971 mullimc 41773 mullimcf 41780 sfprmdvdsmersenne 43645 lincfsuppcl 44396 |
Copyright terms: Public domain | W3C validator |