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 616 . 2 ((𝜑𝜒) → (𝜓𝜒))
3 sylanl1.2 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
42, 3sylan 581 1 (((𝜑𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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
This theorem is referenced by:  adantlll  717  adantllr  718  adantl3r  749  isocnv  7276  f1iun  7877  odi  8527  oeoelem  8546  mapxpen  9088  xadddilem  13214  hashgt23el  14325  pcqmul  16726  infpnlem1  16783  setsn0fun  17046  chpdmat  22193  neitr  22534  hausflimi  23334  nmoix  24096  nmoleub  24098  metdsre  24219  bncssbn  24741  usgr2edg  28161  usgr2edg1  28163  crctcshwlkn0  28769  unoplin  30865  hmoplin  30887  chirredlem1  31335  mdsymlem2  31349  foresf1o  31434  zarcls1  32453  ordtconnlem1  32508  signstfvn  33184  isbasisrelowllem1  35829  isbasisrelowllem2  35830  pibt2  35891  lindsadd  36074  lindsdom  36075  matunitlindflem1  36077  matunitlindflem2  36078  poimirlem25  36106  poimirlem29  36110  heicant  36116  cnambfre  36129  itg2addnclem  36132  ftc1anclem5  36158  ftc1anc  36162  rrnequiv  36297  isfldidl  36530  ispridlc  36532  supxrgelem  43578  supminfxr  43706  itcovalt2lem2  46769  reccot  47210  rectan  47211
  Copyright terms: Public domain W3C validator