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

Theorem syland 604
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 417 . . 3 (𝜑 → (𝜒 → (𝜃𝜏)))
41, 3syld 47 . 2 (𝜑 → (𝜓 → (𝜃𝜏)))
54impd 412 1 (𝜑 → ((𝜓𝜃) → 𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  sylani  605  sylan2d  606  syl2and  609  onfununi  8335  lt2add  11694  nn0seqcvgd  16502  1stcelcls  22946  llyidm  22973  filuni  23370  ballotlemimin  33441  btwnintr  34928  ifscgr  34953  btwnconn1lem12  35007  poimir  36458  cvrntr  38233  goldbachthlem2  46148
  Copyright terms: Public domain W3C validator