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

Theorem syl2ani 607
Description: A syllogism inference. (Contributed by NM, 3-Aug-1999.)
Hypotheses
Ref Expression
syl2ani.1 (𝜑𝜒)
syl2ani.2 (𝜂𝜃)
syl2ani.3 (𝜓 → ((𝜒𝜃) → 𝜏))
Assertion
Ref Expression
syl2ani (𝜓 → ((𝜑𝜂) → 𝜏))

Proof of Theorem syl2ani
StepHypRef Expression
1 syl2ani.1 . 2 (𝜑𝜒)
2 syl2ani.2 . . 3 (𝜂𝜃)
3 syl2ani.3 . . 3 (𝜓 → ((𝜒𝜃) → 𝜏))
42, 3sylan2i 606 . 2 (𝜓 → ((𝜒𝜂) → 𝜏))
51, 4sylani 604 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:  2mo  2645  fvf1pr  7326  frxp  8149  poxp2  8166  mapen  9179  rex2dom  9279  fin1a2lem9  10445  coprmproddvdslem  16695  psss  18637  mgmidmo  18685  aannenlem1  26384  funtransport  36012  cgrxfr  36036  btwnxfr  36037  weiunpo  36447  bj-cbv3tb  36769
  Copyright terms: Public domain W3C validator