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

Theorem sylanl1 671
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 609 . 2 ((𝜑𝜒) → (𝜓𝜒))
3 sylanl1.2 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
42, 3sylan 576 1 (((𝜑𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385
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 199  df-an 386
This theorem is referenced by:  adantlll  710  adantllr  711  isocnv  6806  odi  7897  oeoelem  7916  mapxpen  8366  xadddilem  12369  pcqmul  15888  infpnlem1  15944  setsn0fun  16218  chpdmat  20971  neitr  21310  hausflimi  22109  nmoix  22858  nmoleub  22860  metdsre  22981  bncssbn  23497  usgr2edg1  26437  crctcshwlkn0  27064  sspphOLD  28227  unoplin  29296  hmoplin  29318  chirredlem1  29766  mdsymlem2  29780  foresf1o  29853  ordtconnlem1  30478  isbasisrelowllem1  33693  isbasisrelowllem2  33694  lindsdom  33884  matunitlindflem1  33886  matunitlindflem2  33887  poimirlem25  33915  poimirlem29  33919  heicant  33925  cnambfre  33938  itg2addnclem  33941  ftc1anclem5  33969  ftc1anc  33973  rrnequiv  34113  isfldidl  34346  ispridlc  34348  supxrgelem  40285  supminfxr  40425  reccot  43289  rectan  43290
  Copyright terms: Public domain W3C validator