Theorem syl2an23an 1420

Description: Deduction related to syl3an 1157 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.) (Proof shortened by Wolf Lammen, 28-Jun-2022.)

Hypotheses

Ref	Expression
syl2an23an.1	⊢ (𝜑 → 𝜓)
syl2an23an.2	⊢ (𝜑 → 𝜒)
syl2an23an.3	⊢ ((𝜃 ∧ 𝜑) → 𝜏)
syl2an23an.4	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂)

Assertion

Ref	Expression
syl2an23an	⊢ ((𝜃 ∧ 𝜑) → 𝜂)

Proof of Theorem 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 1419	. 2 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜑)) → 𝜂)
6	5	anabss7 671	1 ⊢ ((𝜃 ∧ 𝜑) → 𝜂)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  nf1const  7319  uztrn  12894  ssfzo12bi  13783  modsumfzodifsn  13966  facdiv  14306  swrdnd  14664  cshwidxmod  14813  nndivdvds  16267  pcz  16885  fldivp1  16901  uffix  23919  relogbmul  26808  umgrvad2edg  29152  crctcshwlkn0  29758  satfsschain  35194  satfdm  35199  satffunlem2  35238