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  962  mpteq12f  4085  opelopabsb  4262  elrelimasn  4996  fvelrnb  5565  fmptco  5684  fconstfvm  5736  f1oiso  5829  canth  5831  mpoeq123  5936  dfoprab4f  6196  fmpox  6203  nnmword  6521  elfi  6972  ltmpig  7340  mul0eqap  8629  qreccl  9644  0fz1  10047  zmodid2  10354  divgcdcoprm0  12103  cnptoprest  13778  txrest  13815  cbvrald  14579