Theorem sylan9bbr 467

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.75  975  mpteq12f  4211  opelopabsb  4402  elrelimasn  5153  fvelrnb  5750  fmptco  5874  fconstfvm  5933  f1oiso  6032  canth  6036  mpoeq123  6147  elovmporab  6289  elovmporab1w  6290  dfoprab4f  6427  fmpox  6436  nnmword  6791  elfi  7305  ltmpig  7706  mul0eqap  9002  qreccl  10051  0fz1  10459  zmodid2  10802  ccatrcl1  11396  divgcdcoprm0  12895  cnptoprest  15389  txrest  15426  uhgreq12g  16415  cbvrald  16914