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

Theorem syl2an3an 1424
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 1421 1 ((𝜑𝜃) → 𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  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 207  df-an 396  df-3an 1089
This theorem is referenced by:  syl2an23an  1425  disjxiun  5140  funcnvtp  6629  fldiv  13900  digit2  14275  ccatass  14626  ccatpfx  14739  swrdswrd  14743  lcmfunsnlem2lem2  16676  cncongr1  16704  lsmval  19666  lsmelval  19667  lmimlbs  21856  mdetdiagid  22606  uncld  23049  hausnei2  23361  uptx  23633  xkohmeo  23823  cnextcn  24075  cnextfres1  24076  nmhmcn  25153  uniioombl  25624  dvcnvlem  26014  dvlip2  26034  taylply2  26409  dvtaylp  26412  taylthlem2  26416  taylthlem2OLD  26417  logbgcd1irr  26837  ftalem2  27117  gausslemma2dlem2  27411  ostth2lem3  27679  wlkeq  29652  eucrctshift  30262  numclwwlk1lem2foalem  30370  numclwlk1lem1  30388  ccatf1  32933  lindsadd  37620  prjspnfv01  42634  prjspner01  42635  omlimcl2  43254  naddwordnexlem3  43412  fmtnofac2lem  47555  isubgr3stgr  47942  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031  itsclc0xyqsolb  48691
  Copyright terms: Public domain W3C validator