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

Theorem syl3anb 1160
Description: A triple syllogism inference. (Contributed by NM, 15-Oct-2005.)
Hypotheses
Ref Expression
syl3anb.1 (𝜑𝜓)
syl3anb.2 (𝜒𝜃)
syl3anb.3 (𝜏𝜂)
syl3anb.4 ((𝜓𝜃𝜂) → 𝜁)
Assertion
Ref Expression
syl3anb ((𝜑𝜒𝜏) → 𝜁)

Proof of Theorem syl3anb
StepHypRef Expression
1 syl3anb.1 . . 3 (𝜑𝜓)
2 syl3anb.2 . . 3 (𝜒𝜃)
3 syl3anb.3 . . 3 (𝜏𝜂)
41, 2, 33anbi123i 1154 . 2 ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))
5 syl3anb.4 . 2 ((𝜓𝜃𝜂) → 𝜁)
64, 5sylbi 217 1 ((𝜑𝜒𝜏) → 𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  w3a 1086
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  df-3an 1088
This theorem is referenced by:  syl3anbr  1161  poxp  8152  infempty  9545  symgsssg  19500  symgfisg  19501  lmodvscl  20893  xrs1mnd  21440  iscnp2  23263  clwwlknccat  30092  slmdvscl  33203  cgr3permute3  36029  cgr3permute1  36030  cgr3permute2  36031  cgr3permute4  36032  cgr3permute5  36033  colinearxfr  36057  grposnOLD  37869  rngunsnply  43158
  Copyright terms: Public domain W3C validator