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

Theorem syl2an3an 1423
Description: syl3an 1161 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.)
Hypotheses
Ref Expression
syl2an3an.1 (𝜑𝜓)
syl2an3an.2 (𝜑𝜒)
syl2an3an.3 (𝜃𝜏)
syl2an3an.4 ((𝜓𝜒𝜏) → 𝜂)
Assertion
Ref Expression
syl2an3an ((𝜑𝜃) → 𝜂)

Proof of Theorem syl2an3an
StepHypRef Expression
1 syl2an3an.1 . . 3 (𝜑𝜓)
2 syl2an3an.2 . . 3 (𝜑𝜒)
3 syl2an3an.3 . . 3 (𝜃𝜏)
4 syl2an3an.4 . . 3 ((𝜓𝜒𝜏) → 𝜂)
51, 2, 3, 4syl3an 1161 . 2 ((𝜑𝜑𝜃) → 𝜂)
653anidm12 1420 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:  syl2an23an  1424  disjxiun  5145  funcnvtp  6609  fldiv  13822  digit2  14196  ccatass  14535  ccatpfx  14648  swrdswrd  14652  lcmfunsnlem2lem2  16573  cncongr1  16601  lsmval  19511  lsmelval  19512  lmimlbs  21383  mdetdiagid  22094  uncld  22537  hausnei2  22849  uptx  23121  xkohmeo  23311  cnextcn  23563  cnextfres1  23564  nmhmcn  24628  uniioombl  25098  dvcnvlem  25485  dvlip2  25504  dvtaylp  25874  taylthlem2  25878  logbgcd1irr  26289  ftalem2  26568  gausslemma2dlem2  26860  ostth2lem3  27128  wlkeq  28881  eucrctshift  29486  numclwwlk1lem2foalem  29594  numclwlk1lem1  29612  ccatf1  32103  lindsadd  36470  prjspnfv01  41363  prjspner01  41364  omlimcl2  41977  naddwordnexlem3  42136  fmtnofac2lem  46223  itsclc0xyqsolb  47410
  Copyright terms: Public domain W3C validator