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  964  mpteq12f  4110  opelopabsb  4291  elrelimasn  5032  fvelrnb  5605  fmptco  5725  fconstfvm  5777  f1oiso  5870  canth  5872  mpoeq123  5978  elovmporab  6120  elovmporab1w  6121  dfoprab4f  6248  fmpox  6255  nnmword  6573  elfi  7032  ltmpig  7401  mul0eqap  8691  qreccl  9710  0fz1  10114  zmodid2  10426  divgcdcoprm0  12242  cnptoprest  14418  txrest  14455  cbvrald  15350