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

Theorem syland 498
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 452 . . 3 (𝜑 → (𝜒 → (𝜃𝜏)))
41, 3syld 47 . 2 (𝜑 → (𝜓 → (𝜃𝜏)))
54impd 447 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:  sylan2d  499  syl2and  500  sylani  685  onfununi  7383  lt2add  10457  nn0seqcvgd  15207  1stcelcls  21174  llyidm  21201  filuni  21599  ballotlemimin  30348  btwnintr  31768  ifscgr  31793  btwnconn1lem12  31847  poimir  33074  cvrntr  34191  goldbachthlem2  40757
  Copyright terms: Public domain W3C validator