Theorem sylan9bbr 461

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 460	. 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  958  mpteq12f  4070  opelopabsb  4246  elreimasng  4979  fvelrnb  5547  fmptco  5666  fconstfvm  5718  f1oiso  5809  canth  5811  mpoeq123  5916  dfoprab4f  6176  fmpox  6183  nnmword  6501  elfi  6952  ltmpig  7305  mul0eqap  8592  qreccl  9605  0fz1  10005  zmodid2  10312  divgcdcoprm0  12059  cnptoprest  13118  txrest  13155  cbvrald  13908