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  4113  opelopabsb  4294  elrelimasn  5035  fvelrnb  5608  fmptco  5728  fconstfvm  5780  f1oiso  5873  canth  5875  mpoeq123  5981  elovmporab  6123  elovmporab1w  6124  dfoprab4f  6251  fmpox  6258  nnmword  6576  elfi  7037  ltmpig  7406  mul0eqap  8697  qreccl  9716  0fz1  10120  zmodid2  10444  divgcdcoprm0  12269  cnptoprest  14475  txrest  14512  cbvrald  15434