![]() |
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 7304 uztrn 12842 ssfzo12bi 13729 modsumfzodifsn 13911 facdiv 14249 swrdnd 14606 cshwidxmod 14755 nndivdvds 16208 pcz 16816 fldivp1 16832 uffix 23432 relogbmul 26289 umgrvad2edg 28508 crctcshwlkn0 29113 satfsschain 34424 satfdm 34429 satffunlem2 34468 |
Copyright terms: Public domain | W3C validator |