![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl2an23an | Structured version Visualization version GIF version |
Description: Deduction related to syl3an 1160 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.) (Proof shortened by Wolf Lammen, 28-Jun-2022.) |
Ref | Expression |
---|---|
syl2an23an.1 | ⊢ (𝜑 → 𝜓) |
syl2an23an.2 | ⊢ (𝜑 → 𝜒) |
syl2an23an.3 | ⊢ ((𝜃 ∧ 𝜑) → 𝜏) |
syl2an23an.4 | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂) |
Ref | Expression |
---|---|
syl2an23an | ⊢ ((𝜃 ∧ 𝜑) → 𝜂) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2an23an.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | syl2an23an.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | syl2an23an.3 | . . 3 ⊢ ((𝜃 ∧ 𝜑) → 𝜏) | |
4 | syl2an23an.4 | . . 3 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂) | |
5 | 1, 2, 3, 4 | syl2an3an 1422 | . 2 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜑)) → 𝜂) |
6 | 5 | anabss7 671 | 1 ⊢ ((𝜃 ∧ 𝜑) → 𝜂) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ 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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: nf1const 7301 uztrn 12839 ssfzo12bi 13726 modsumfzodifsn 13908 facdiv 14246 swrdnd 14603 cshwidxmod 14752 nndivdvds 16205 pcz 16813 fldivp1 16829 uffix 23424 relogbmul 26279 umgrvad2edg 28467 crctcshwlkn0 29072 satfsschain 34350 satfdm 34355 satffunlem2 34394 |
Copyright terms: Public domain | W3C validator |