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

Theorem syl3anb 1271
Description: A triple syllogism inference. (Contributed by NM, 15-Oct-2005.)
Hypotheses
Ref Expression
syl3anb.1  |-  ( ph  <->  ps )
syl3anb.2  |-  ( ch  <->  th )
syl3anb.3  |-  ( ta  <->  et )
syl3anb.4  |-  ( ( ps  /\  th  /\  et )  ->  ze )
Assertion
Ref Expression
syl3anb  |-  ( (
ph  /\  ch  /\  ta )  ->  ze )

Proof of Theorem syl3anb
StepHypRef Expression
1 syl3anb.1 . . 3  |-  ( ph  <->  ps )
2 syl3anb.2 . . 3  |-  ( ch  <->  th )
3 syl3anb.3 . . 3  |-  ( ta  <->  et )
41, 2, 33anbi123i 1185 . 2  |-  ( (
ph  /\  ch  /\  ta ) 
<->  ( ps  /\  th  /\  et ) )
5 syl3anb.4 . 2  |-  ( ( ps  /\  th  /\  et )  ->  ze )
64, 5sylbi 195 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ze )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  syl3anbr  1272  poxp  6892  symgsssg  16288  symgfisg  16289  lmodvscl  17312  xrs1mnd  18224  iscnp2  19506  nb3grapr  24129  grposn  24893  slmdvscl  27419  cgr3permute3  29274  cgr3permute1  29275  cgr3permute2  29276  cgr3permute4  29277  cgr3permute5  29278  colinearxfr  29302  rngunsnply  30727
  Copyright terms: Public domain W3C validator