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

Theorem syl2an23an 1423
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 1422 . 2 ((𝜑 ∧ (𝜃𝜑)) → 𝜂)
65anabss7 671 1 ((𝜃𝜑) → 𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  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 206  df-an 397  df-3an 1089
This theorem is referenced by:  nf1const  7304  uztrn  12842  ssfzo12bi  13729  modsumfzodifsn  13911  facdiv  14249  swrdnd  14606  cshwidxmod  14755  nndivdvds  16208  pcz  16816  fldivp1  16832  uffix  23432  relogbmul  26289  umgrvad2edg  28508  crctcshwlkn0  29113  satfsschain  34424  satfdm  34429  satffunlem2  34468
  Copyright terms: Public domain W3C validator