Theorem syl3an3b 1364

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

Ref	Expression
syl3an3b.1	|- ( ph <-> th )
syl3an3b.2	|- ( ( ps /\ ch /\ th ) -> ta )

Assertion

Ref	Expression
syl3an3b	|- ( ( ps /\ ch /\ ph ) -> ta )

Proof of Theorem syl3an3b

Step	Hyp	Ref	Expression
1		syl3an3b.1	. . 3 |- ( ph <-> th )
2	1	biimpi 206	. 2 |- ( ph -> th )
3		syl3an3b.2	. 2 |- ( ( ps /\ ch /\ th ) -> ta )
4	2, 3	syl3an3 1361	1 |- ( ( ps /\ ch /\ ph ) -> ta )

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:  fresaunres1  6077  fvun2  6270  nnmsucr  7705  xrlttr  11973  iccdil  12310  icccntr  12312  absexpz  14045  posglbd  17150  f1omvdco3  17869  isdrngd  18772  unicld  20850  2ndcdisj2  21260  logrec  24501  cdj3lem3  29297  bnj563  30813  bnj1033  31037  stoweidlem14  40231