![]() |
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 1420 | 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: syl2an23an 1424 disjxiun 5145 funcnvtp 6609 fldiv 13822 digit2 14196 ccatass 14535 ccatpfx 14648 swrdswrd 14652 lcmfunsnlem2lem2 16573 cncongr1 16601 lsmval 19511 lsmelval 19512 lmimlbs 21383 mdetdiagid 22094 uncld 22537 hausnei2 22849 uptx 23121 xkohmeo 23311 cnextcn 23563 cnextfres1 23564 nmhmcn 24628 uniioombl 25098 dvcnvlem 25485 dvlip2 25504 dvtaylp 25874 taylthlem2 25878 logbgcd1irr 26289 ftalem2 26568 gausslemma2dlem2 26860 ostth2lem3 27128 wlkeq 28881 eucrctshift 29486 numclwwlk1lem2foalem 29594 numclwlk1lem1 29612 ccatf1 32103 lindsadd 36470 prjspnfv01 41363 prjspner01 41364 omlimcl2 41977 naddwordnexlem3 42136 fmtnofac2lem 46223 itsclc0xyqsolb 47410 |
Copyright terms: Public domain | W3C validator |