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

Theorem sylanl1 683
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 591 . 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 197  df-an 385
This theorem is referenced by:  adantlll  754  adantllr  755  isocnv  6620  odi  7704  oeoelem  7723  mapxpen  8167  xadddilem  12162  pcqmul  15605  infpnlem1  15661  setsn0fun  15942  chpdmat  20694  neitr  21032  hausflimi  21831  nmoix  22580  nmoleub  22582  metdsre  22703  usgr2edg1  26149  crctcshwlkn0  26769  sspph  27838  unoplin  28907  hmoplin  28929  chirredlem1  29377  mdsymlem2  29391  foresf1o  29469  ordtconnlem1  30098  isbasisrelowllem1  33333  isbasisrelowllem2  33334  lindsdom  33533  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem25  33564  poimirlem29  33568  heicant  33574  cnambfre  33588  itg2addnclem  33591  ftc1anclem5  33619  ftc1anc  33623  rrnequiv  33764  isfldidl  33997  ispridlc  33999  supxrgelem  39866  supminfxr  40007  reccot  42827  rectan  42828
  Copyright terms: Public domain W3C validator