Theorem syl2an23an 1426

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  nf1const  7250  uztrn  12795  ssfzo12bi  13705  modsumfzodifsn  13895  facdiv  14238  swrdnd  14606  cshwidxmod  14754  nndivdvds  16219  pcz  16841  fldivp1  16857  uffix  23895  relogbmul  26758  umgrvad2edg  29301  crctcshwlkn0  29909  satfsschain  35567  satfdm  35572  satffunlem2  35611  modmkpkne  47812  pgn4cyclex  48599