Theorem syl2an23an 1425

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.)

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 1424	. 2 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜑)) → 𝜂)
6	5	anabss7 673	1 ⊢ ((𝜃 ∧ 𝜑) → 𝜂)

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  7302  uztrn  12875  ssfzo12bi  13782  modsumfzodifsn  13967  facdiv  14310  swrdnd  14677  cshwidxmod  14826  nndivdvds  16286  pcz  16906  fldivp1  16922  uffix  23864  relogbmul  26744  umgrvad2edg  29197  crctcshwlkn0  29808  satfsschain  35391  satfdm  35396  satffunlem2  35435