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

Theorem syl3anb 1227
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 1142 . 2  |-  ( (
ph  /\  ch  /\  ta ) 
<->  ( ps  /\  th  /\  et ) )
5 syl3anb.4 . 2  |-  ( ( ps  /\  th  /\  et )  ->  ze )
64, 5sylbi 188 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936
This theorem is referenced by:  syl3anbr  1228  poxp  6458  lmodvscl  15967  xrs1mnd  16736  iscnp2  17303  nb3grapr  21462  grposn  21803  cgr3permute3  25981  cgr3permute1  25982  cgr3permute2  25983  cgr3permute4  25984  cgr3permute5  25985  colinearxfr  26009  rngunsnply  27355  symgsssg  27385  symgfisg  27386
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator