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

Theorem sylanl1 682
 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 592 . 2 ((𝜑𝜒) → (𝜓𝜒))
3 sylanl1.2 . 2 (((𝜓𝜒) ∧ 𝜃) → 𝜏)
42, 3sylan 488 1 (((𝜑𝜒) ∧ 𝜃) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384 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 386 This theorem is referenced by:  adantlll  754  adantllr  755  isocnv  6577  odi  7656  oeoelem  7675  mapxpen  8123  xadddilem  12121  pcqmul  15552  infpnlem1  15608  setsn0fun  15889  chpdmat  20640  neitr  20978  hausflimi  21778  nmoix  22527  nmoleub  22529  metdsre  22650  usgr2edg1  26098  crctcshwlkn0  26707  sspph  27694  unoplin  28763  hmoplin  28785  chirredlem1  29233  mdsymlem2  29247  foresf1o  29327  ordtconnlem1  29955  isbasisrelowllem1  33183  isbasisrelowllem2  33184  lindsdom  33383  matunitlindflem1  33385  matunitlindflem2  33386  poimirlem25  33414  poimirlem29  33418  heicant  33424  cnambfre  33438  itg2addnclem  33441  ftc1anclem5  33469  ftc1anc  33473  rrnequiv  33614  isfldidl  33847  ispridlc  33849  supxrgelem  39372  supminfxr  39513  reccot  42270  rectan  42271
 Copyright terms: Public domain W3C validator