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

Theorem syland 603
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 415 . . 3 (𝜑 → (𝜒 → (𝜃𝜏)))
41, 3syld 47 . 2 (𝜑 → (𝜓 → (𝜃𝜏)))
54impd 410 1 (𝜑 → ((𝜓𝜃) → 𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  sylani  604  sylan2d  605  syl2and  608  onfununi  8379  fodomfir  9365  lt2add  11745  nn0seqcvgd  16603  1stcelcls  23484  llyidm  23511  filuni  23908  ballotlemimin  34486  btwnintr  36000  ifscgr  36025  btwnconn1lem12  36079  poimir  37639  cvrntr  39407  goldbachthlem2  47470
  Copyright terms: Public domain W3C validator