Theorem sylan9bbr 463

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)

Hypotheses

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

Assertion

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

Proof of Theorem sylan9bbr

Step	Hyp	Ref	Expression
1		sylan9bbr.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2		sylan9bbr.2	. . 3 |- ( th -> ( ch <-> ta ) )
3	1, 2	sylan9bb 462	. 2 |- ( ( ph /\ th ) -> ( ps <-> ta ) )
4	3	ancoms 268	1 |- ( ( th /\ ph ) -> ( ps <-> ta ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.75  971  mpteq12f  4174  opelopabsb  4360  elrelimasn  5109  fvelrnb  5702  fmptco  5821  fconstfvm  5880  f1oiso  5977  canth  5979  mpoeq123  6090  elovmporab  6232  elovmporab1w  6233  dfoprab4f  6365  fmpox  6374  nnmword  6729  elfi  7230  ltmpig  7619  mul0eqap  8909  qreccl  9937  0fz1  10342  zmodid2  10677  ccatrcl1  11257  divgcdcoprm0  12753  cnptoprest  15050  txrest  15087  uhgreq12g  16017  cbvrald  16506