Theorem syl3an3b 1135

Description: A syllogism inference.

Hypotheses

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

Assertion

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

Proof of Theorem syl3an3b

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

Syntax hints:   -> wi 3   <-> wb 163   /\ w3a 858

This theorem is referenced by:  nnmsucr 5295  nnmsucrOLD 5296  ordtypelem7 5690  xrlttr 6728  supxrre 7292  basgen 8910  intcld 8956  cdj3lem3 12010  bnj559 12539  bnj1033 13384  suplub2 14616  ordtypelem7OLD 15381  topbasfne 15499  iccdil 15861  icccntr 15863

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860

Copyright terms: Public domain