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  2648  fvf1pr  7327  frxp  8151  poxp2  8168  mapen  9181  rex2dom  9282  fin1a2lem9  10448  coprmproddvdslem  16699  psss  18625  mgmidmo  18673  aannenlem1  26370  funtransport  36032  cgrxfr  36056  btwnxfr  36057  weiunpo  36466  bj-cbv3tb  36788
  Copyright terms: Public domain W3C validator