MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2an23an Structured version   Visualization version   GIF version

Theorem syl2an23an 1424
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
StepHypRef Expression
1 syl2an23an.1 . . 3 (𝜑𝜓)
2 syl2an23an.2 . . 3 (𝜑𝜒)
3 syl2an23an.3 . . 3 ((𝜃𝜑) → 𝜏)
4 syl2an23an.4 . . 3 ((𝜓𝜒𝜏) → 𝜂)
51, 2, 3, 4syl2an3an 1423 . 2 ((𝜑 ∧ (𝜃𝜑)) → 𝜂)
65anabss7 672 1 ((𝜃𝜑) → 𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  nf1const  7302  uztrn  12840  ssfzo12bi  13727  modsumfzodifsn  13909  facdiv  14247  swrdnd  14604  cshwidxmod  14753  nndivdvds  16206  pcz  16814  fldivp1  16830  uffix  23425  relogbmul  26282  umgrvad2edg  28470  crctcshwlkn0  29075  satfsschain  34355  satfdm  34360  satffunlem2  34399
  Copyright terms: Public domain W3C validator