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

Theorem syl3anb 1273
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 1186 . 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 974
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 369  df-3an 976
This theorem is referenced by:  syl3anbr  1274  poxp  6895  symgsssg  16814  symgfisg  16815  lmodvscl  17847  xrs1mnd  18774  iscnp2  20031  nb3grapr  24857  grposn  25617  slmdvscl  28195  cgr3permute3  30372  cgr3permute1  30373  cgr3permute2  30374  cgr3permute4  30375  cgr3permute5  30376  colinearxfr  30400  rngunsnply  35466
  Copyright terms: Public domain W3C validator