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

Theorem syl3anb 1161
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 1155 . 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  1162  poxp  8154  infempty  9548  symgsssg  19486  symgfisg  19487  lmodvscl  20877  xrs1mnd  21423  iscnp2  23248  clwwlknccat  30083  slmdvscl  33221  cgr3permute3  36049  cgr3permute1  36050  cgr3permute2  36051  cgr3permute4  36052  cgr3permute5  36053  colinearxfr  36077  grposnOLD  37890  rngunsnply  43186
  Copyright terms: Public domain W3C validator