Theorem sylan9bbr 454

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 453	. 2 |- ( ( ph /\ th ) -> ( ps <-> ta ) )
4	3	ancoms 266	1 |- ( ( th /\ ph ) -> ( ps <-> ta ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.75  914  mpteq12f  3948  opelopabsb  4120  elreimasng  4841  fvelrnb  5401  fmptco  5518  fconstfvm  5570  f1oiso  5659  mpoeq123  5762  dfoprab4f  6021  fmpox  6028  nnmword  6344  ltmpig  7048  mul0eqap  8292  qreccl  9284  0fz1  9666  zmodid2  9966  divgcdcoprm0  11575  cnptoprest  12189  txrest  12226  cbvrald  12576