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

Theorem sylanl1 676
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 614 . 2 ((𝜑𝜒) → (𝜓𝜒))
3 sylanl1.2 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
42, 3sylan 580 1 (((𝜑𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  adantlll  714  adantllr  715  adantl3r  746  isocnv  6946  f1iun  7501  odi  8055  oeoelem  8074  mapxpen  8530  xadddilem  12537  hashgt23el  13633  pcqmul  16019  infpnlem1  16075  setsn0fun  16349  chpdmat  21133  neitr  21472  hausflimi  22272  nmoix  23021  nmoleub  23023  metdsre  23144  bncssbn  23660  usgr2edg  26675  usgr2edg1  26677  crctcshwlkn0  27286  unoplin  29388  hmoplin  29410  chirredlem1  29858  mdsymlem2  29872  foresf1o  29957  ordtconnlem1  30784  isbasisrelowllem1  34186  isbasisrelowllem2  34187  pibt2  34248  lindsadd  34435  lindsdom  34436  matunitlindflem1  34438  matunitlindflem2  34439  poimirlem25  34467  poimirlem29  34471  heicant  34477  cnambfre  34490  itg2addnclem  34493  ftc1anclem5  34521  ftc1anc  34525  rrnequiv  34664  isfldidl  34897  ispridlc  34899  supxrgelem  41165  supminfxr  41301  reccot  44357  rectan  44358
  Copyright terms: Public domain W3C validator