Theorem syl3anb 1369

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

Step	Hyp	Ref	Expression
1		syl3anb.1	. . 3 |- ( ph <-> ps )
2		syl3anb.2	. . 3 |- ( ch <-> th )
3		syl3anb.3	. . 3 |- ( ta <-> et )
4	1, 2, 3	3anbi123i 1251	. 2 |- ( ( ph /\ ch /\ ta ) <-> ( ps /\ th /\ et ) )
5		syl3anb.4	. 2 |- ( ( ps /\ th /\ et ) -> ze )
6	4, 5	sylbi 207	1 |- ( ( ph /\ ch /\ ta ) -> ze )

Syntax hints:   -> wi 4   <-> wb 196   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  syl3anbr  1370  poxp  7289  infempty  8412  symgsssg  17887  symgfisg  17888  lmodvscl  18880  xrs1mnd  19784  iscnp2  21043  slmdvscl  29767  cgr3permute3  32154  cgr3permute1  32155  cgr3permute2  32156  cgr3permute4  32157  cgr3permute5  32158  colinearxfr  32182  grposnOLD  33681  rngunsnply  37743