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

Theorem sylanl1 680
 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 590 . 2 ((𝜑𝜒) → (𝜓𝜒))
3 sylanl1.2 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
42, 3sylan 487 1 (((𝜑𝜒) ∧ 𝜃) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  adantlll  750  adantllr  751  isocnv  6480  odi  7546  oeoelem  7565  mapxpen  8011  xadddilem  11996  pcqmul  15396  infpnlem1  15452  chpdmat  20465  neitr  20794  hausflimi  21594  nmoix  22343  nmoleub  22345  metdsre  22464  pthdepisspth  26104  extwwlkfab  26617  sspph  27094  unoplin  28163  hmoplin  28185  chirredlem1  28633  mdsymlem2  28647  foresf1o  28727  ordtconlem1  29298  isbasisrelowllem1  32379  isbasisrelowllem2  32380  lindsdom  32573  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem25  32604  poimirlem29  32608  heicant  32614  cnambfre  32628  itg2addnclem  32631  ftc1anclem5  32659  ftc1anc  32663  rrnequiv  32804  isfldidl  33037  ispridlc  33039  supxrgelem  38494  usgr2edg1  40439  crctcsh1wlkn0  41024  reccot  42298  rectan  42299
 Copyright terms: Public domain W3C validator