Theorem syl2an23an 1422

Description: Deduction related to syl3an 1159 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 1421	. 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  7324  uztrn  12894  ssfzo12bi  13797  modsumfzodifsn  13982  facdiv  14323  swrdnd  14689  cshwidxmod  14838  nndivdvds  16296  pcz  16915  fldivp1  16931  uffix  23945  relogbmul  26835  umgrvad2edg  29245  crctcshwlkn0  29851  satfsschain  35349  satfdm  35354  satffunlem2  35393