| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > syl2an3an | Structured version Visualization version GIF version | ||
| Description: syl3an 1161 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.) |
| Ref | Expression |
|---|---|
| syl2an3an.1 | ⊢ (𝜑 → 𝜓) |
| syl2an3an.2 | ⊢ (𝜑 → 𝜒) |
| syl2an3an.3 | ⊢ (𝜃 → 𝜏) |
| syl2an3an.4 | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂) |
| Ref | Expression |
|---|---|
| syl2an3an | ⊢ ((𝜑 ∧ 𝜃) → 𝜂) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syl2an3an.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
| 2 | syl2an3an.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
| 3 | syl2an3an.3 | . . 3 ⊢ (𝜃 → 𝜏) | |
| 4 | syl2an3an.4 | . . 3 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂) | |
| 5 | 1, 2, 3, 4 | syl3an 1161 | . 2 ⊢ ((𝜑 ∧ 𝜑 ∧ 𝜃) → 𝜂) |
| 6 | 5 | 3anidm12 1421 | 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: syl2an23an 1425 disjxiun 5140 funcnvtp 6629 fldiv 13900 digit2 14275 ccatass 14626 ccatpfx 14739 swrdswrd 14743 lcmfunsnlem2lem2 16676 cncongr1 16704 lsmval 19666 lsmelval 19667 lmimlbs 21856 mdetdiagid 22606 uncld 23049 hausnei2 23361 uptx 23633 xkohmeo 23823 cnextcn 24075 cnextfres1 24076 nmhmcn 25153 uniioombl 25624 dvcnvlem 26014 dvlip2 26034 taylply2 26409 dvtaylp 26412 taylthlem2 26416 taylthlem2OLD 26417 logbgcd1irr 26837 ftalem2 27117 gausslemma2dlem2 27411 ostth2lem3 27679 wlkeq 29652 eucrctshift 30262 numclwwlk1lem2foalem 30370 numclwlk1lem1 30388 ccatf1 32933 lindsadd 37620 prjspnfv01 42634 prjspner01 42635 omlimcl2 43254 naddwordnexlem3 43412 fmtnofac2lem 47555 isubgr3stgr 47942 gpgnbgrvtx0 48030 gpgnbgrvtx1 48031 itsclc0xyqsolb 48691 |
| Copyright terms: Public domain | W3C validator |