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

Theorem syland 497
 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 451 . . 3 (𝜑 → (𝜒 → (𝜃𝜏)))
41, 3syld 46 . 2 (𝜑 → (𝜓 → (𝜃𝜏)))
54impd 446 1 (𝜑 → ((𝜓𝜃) → 𝜏))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  sylan2d  498  syl2and  499  sylani  684  onfununi  7325  lt2add  10392  nn0seqcvgd  15121  1stcelcls  21074  llyidm  21101  filuni  21499  ballotlemimin  29894  btwnintr  31296  ifscgr  31321  btwnconn1lem12  31375  poimir  32612  cvrntr  33729  goldbachthlem2  39996
 Copyright terms: Public domain W3C validator