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

Theorem syland 590
Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
Hypotheses
Ref Expression
syland.1 (𝜑 → (𝜓𝜒))
syland.2 (𝜑 → ((𝜒𝜃) → 𝜏))
Assertion
Ref Expression
syland (𝜑 → ((𝜓𝜃) → 𝜏))

Proof of Theorem syland
StepHypRef Expression
1 syland.1 . . 3 (𝜑 → (𝜓𝜒))
2 syland.2 . . . 4 (𝜑 → ((𝜒𝜃) → 𝜏))
32expd 400 . . 3 (𝜑 → (𝜒 → (𝜃𝜏)))
41, 3syld 47 . 2 (𝜑 → (𝜓 → (𝜃𝜏)))
54impd 396 1 (𝜑 → ((𝜓𝜃) → 𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  sylani  591  sylan2d  592  syl2and  595  onfununi  7589  lt2add  10713  nn0seqcvgd  15484  1stcelcls  21478  llyidm  21505  filuni  21902  ballotlemimin  30900  btwnintr  32456  ifscgr  32481  btwnconn1lem12  32535  poimir  33768  cvrntr  35226  goldbachthlem2  41979
  Copyright terms: Public domain W3C validator