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

Theorem sylanl1 679
Description: A syllogism inference. (Contributed by NM, 10-Mar-2005.)
Hypotheses
Ref Expression
sylanl1.1 (𝜑𝜓)
sylanl1.2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
Assertion
Ref Expression
sylanl1 (((𝜑𝜒) ∧ 𝜃) → 𝜏)

Proof of Theorem sylanl1
StepHypRef Expression
1 sylanl1.1 . . 3 (𝜑𝜓)
21anim1i 589 . 2 ((𝜑𝜒) → (𝜓𝜒))
3 sylanl1.2 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
42, 3sylan 486 1 (((𝜑𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  adantlll  749  adantllr  750  isocnv  6454  odi  7519  oeoelem  7538  mapxpen  7984  xadddilem  11949  pcqmul  15338  infpnlem1  15394  chpdmat  20403  neitr  20732  hausflimi  21532  nmoix  22271  nmoleub  22273  metdsre  22391  pthdepisspth  25866  extwwlkfab  26379  sspph  26896  unoplin  27965  hmoplin  27987  chirredlem1  28435  mdsymlem2  28449  foresf1o  28529  ordtconlem1  29100  isbasisrelowllem1  32178  isbasisrelowllem2  32179  lindsdom  32372  matunitlindflem1  32374  matunitlindflem2  32375  poimirlem25  32403  poimirlem29  32407  heicant  32413  cnambfre  32427  itg2addnclem  32430  ftc1anclem5  32458  ftc1anc  32462  rrnequiv  32603  isfldidl  32836  ispridlc  32838  supxrgelem  38294  usgr2edg1  40437  crctcsh1wlkn0  41022  reccot  42257  rectan  42258
  Copyright terms: Public domain W3C validator