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

Theorem syl3anb 1225
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 1140 . 2  |-  ( (
ph  /\  ch  /\  ta ) 
<->  ( ps  /\  th  /\  et ) )
5 syl3anb.4 . 2  |-  ( ( ps  /\  th  /\  et )  ->  ze )
64, 5sylbi 187 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  syl3anbr  1226  poxp  6227  lmodvscl  15644  xrs1mnd  16409  iscnp2  16969  grposn  20882  cgr3permute3  24670  cgr3permute1  24671  cgr3permute2  24672  cgr3permute4  24673  cgr3permute5  24674  colinearxfr  24698  conttnf2  25562  cmptdst  25568  rngunsnply  27378  symgsssg  27408  symgfisg  27409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator