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  7072  f1iun  7634  odi  8194  oeoelem  8213  mapxpen  8671  xadddilem  12675  hashgt23el  13773  pcqmul  16178  infpnlem1  16234  setsn0fun  16508  chpdmat  21377  neitr  21716  hausflimi  22516  nmoix  23265  nmoleub  23267  metdsre  23388  bncssbn  23904  usgr2edg  26919  usgr2edg1  26921  crctcshwlkn0  27526  unoplin  29624  hmoplin  29646  chirredlem1  30094  mdsymlem2  30108  foresf1o  30192  ordtconnlem1  31066  signstfvn  31738  isbasisrelowllem1  34518  isbasisrelowllem2  34519  pibt2  34580  lindsadd  34766  lindsdom  34767  matunitlindflem1  34769  matunitlindflem2  34770  poimirlem25  34798  poimirlem29  34802  heicant  34808  cnambfre  34821  itg2addnclem  34824  ftc1anclem5  34852  ftc1anc  34856  rrnequiv  34994  isfldidl  35227  ispridlc  35229  supxrgelem  41481  supminfxr  41616  reccot  44785  rectan  44786
  Copyright terms: Public domain W3C validator