Theorem syl2an23an 1450

Description: Deduction related to syl3an 1178 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 1449	. 2 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜑)) → 𝜂)
6	5	anabss7 686	1 ⊢ ((𝜃 ∧ 𝜑) → 𝜂)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  nf1const  7312  uztrn  12983  ssfzo12bi  13896  modsumfzodifsn  14087  facdiv  14431  swrdnd  14804  cshwidxmod  14954  nndivdvds  16431  pcz  17059  fldivp1  17075  uffix  24240  relogbmul  27105  umgrvad2edg  29794  crctcshwlkn0  30410  satfsschain  36171  satfdm  36176  satffunlem2  36215  modmkpkne  48480  pgn4cyclex  49267