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

Theorem syl3anb 1163
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 1157 . 2 ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))
5 syl3anb.4 . 2 ((𝜓𝜃𝜂) → 𝜁)
64, 5sylbi 207 1 ((𝜑𝜒𝜏) → 𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1070
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 197  df-an 383  df-3an 1072
This theorem is referenced by:  syl3anbr  1164  poxp  7439  infempty  8567  symgsssg  18093  symgfisg  18094  lmodvscl  19089  xrs1mnd  19998  iscnp2  21263  clwwlknccat  27218  slmdvscl  30101  cgr3permute3  32485  cgr3permute1  32486  cgr3permute2  32487  cgr3permute4  32488  cgr3permute5  32489  colinearxfr  32513  grposnOLD  34006  rngunsnply  38262
  Copyright terms: Public domain W3C validator