Theorem sylan9bbr 458

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 457	. 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-mp 5  ax-1 6  ax-2 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  946  mpteq12f  4003  opelopabsb  4177  elreimasng  4900  fvelrnb  5462  fmptco  5579  fconstfvm  5631  f1oiso  5720  mpoeq123  5823  dfoprab4f  6084  fmpox  6091  nnmword  6407  elfi  6852  ltmpig  7140  mul0eqap  8424  qreccl  9427  0fz1  9818  zmodid2  10118  divgcdcoprm0  11771  cnptoprest  12397  txrest  12434  cbvrald  12984