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

Theorem syl2an23an 1420
 Description: Deduction related to syl3an 1157 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 1419 . 2 ((𝜑 ∧ (𝜃𝜑)) → 𝜂)
65anabss7 672 1 ((𝜃𝜑) → 𝜂)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  nf1const  7042  uztrn  12253  ssfzo12bi  13131  modsumfzodifsn  13311  facdiv  13647  swrdnd  14011  cshwidxmod  14160  nndivdvds  15611  pcz  16210  fldivp1  16226  uffix  22529  relogbmul  25366  umgrvad2edg  27006  crctcshwlkn0  27610  satfsschain  32719  satfdm  32724  satffunlem2  32763
 Copyright terms: Public domain W3C validator