Theorem syl2anbr 497

Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)

Hypotheses

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

Assertion

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

Proof of Theorem syl2anbr

Step	Hyp	Ref	Expression
1		syl2anbr.2	. 2 |- ( ch <-> ta )
2		syl2anbr.1	. . 3 |- ( ps <-> ph )
3		syl2anbr.3	. . 3 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylanbr 490	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	sylan2br 493	1 |- ( ( ph /\ ta ) -> th )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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

This theorem is referenced by:  sylancbr  700  reusv2  4874  tz6.12  6211  r1ord3  8645  brdom7disj  9353  brdom6disj  9354  alephadd  9399  ltresr  9961  divmuldiv  10725  fnn0ind  11476  rexanuz  14085  nprmi  15402  lsmvalx  18054  cncfval  22691  angval  24531  amgmlem  24716  sspval  27578  sshjval  28209  sshjval3  28213  hosmval  28594  hodmval  28596  hfsmval  28597  broutsideof3  32233  mptsnunlem  33185  relowlpssretop  33212