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 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
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 673 1 ((𝜃𝜑) → 𝜂)
Colors of variables: wff setvar class
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  7325  uztrn  12897  ssfzo12bi  13801  modsumfzodifsn  13986  facdiv  14327  swrdnd  14693  cshwidxmod  14842  nndivdvds  16300  pcz  16920  fldivp1  16936  uffix  23930  relogbmul  26821  umgrvad2edg  29231  crctcshwlkn0  29842  satfsschain  35370  satfdm  35375  satffunlem2  35414
  Copyright terms: Public domain W3C validator