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 1162 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 1424 | . 2 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜑)) → 𝜂) |
6 | 5 | anabss7 673 | 1 ⊢ ((𝜃 ∧ 𝜑) → 𝜂) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: nf1const 7103 uztrn 12439 ssfzo12bi 13320 modsumfzodifsn 13500 facdiv 13836 swrdnd 14202 cshwidxmod 14351 nndivdvds 15805 pcz 16415 fldivp1 16431 uffix 22790 relogbmul 25632 umgrvad2edg 27273 crctcshwlkn0 27877 satfsschain 33011 satfdm 33016 satffunlem2 33055 |
Copyright terms: Public domain | W3C validator |