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  6243  lmodvscl  15660  xrs1mnd  16425  iscnp2  16985  grposn  20898  cgr3permute3  24742  cgr3permute1  24743  cgr3permute2  24744  cgr3permute4  24745  cgr3permute5  24746  colinearxfr  24770  conttnf2  25665  cmptdst  25671  rngunsnply  27481  symgsssg  27511  symgfisg  27512  nb3grapr  28289
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