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

Theorem syland 606
 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 420 . . 3 (𝜑 → (𝜒 → (𝜃𝜏)))
41, 3syld 47 . 2 (𝜑 → (𝜓 → (𝜃𝜏)))
54impd 415 1 (𝜑 → ((𝜓𝜃) → 𝜏))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 400 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 210  df-an 401 This theorem is referenced by:  sylani  607  sylan2d  608  syl2and  611  onfununi  7989  lt2add  11156  nn0seqcvgd  15959  1stcelcls  22154  llyidm  22181  filuni  22578  ballotlemimin  31984  btwnintr  33863  ifscgr  33888  btwnconn1lem12  33942  poimir  35363  cvrntr  36994  goldbachthlem2  44424
 Copyright terms: Public domain W3C validator