![]() |
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 1161 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 1423 | . 2 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜑)) → 𝜂) |
6 | 5 | anabss7 672 | 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: nf1const 7302 uztrn 12840 ssfzo12bi 13727 modsumfzodifsn 13909 facdiv 14247 swrdnd 14604 cshwidxmod 14753 nndivdvds 16206 pcz 16814 fldivp1 16830 uffix 23425 relogbmul 26282 umgrvad2edg 28470 crctcshwlkn0 29075 satfsschain 34355 satfdm 34360 satffunlem2 34399 |
Copyright terms: Public domain | W3C validator |