|   | 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 1423 | . 2 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜑)) → 𝜂) | 
| 6 | 5 | anabss7 673 | 1 ⊢ ((𝜃 ∧ 𝜑) → 𝜂) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 | 
| 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 207 df-an 396 df-3an 1088 | 
| This theorem is referenced by: nf1const 7325 uztrn 12897 ssfzo12bi 13801 modsumfzodifsn 13986 facdiv 14327 swrdnd 14693 cshwidxmod 14842 nndivdvds 16300 pcz 16920 fldivp1 16936 uffix 23930 relogbmul 26821 umgrvad2edg 29231 crctcshwlkn0 29842 satfsschain 35370 satfdm 35375 satffunlem2 35414 | 
| Copyright terms: Public domain | W3C validator |