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  965  mpteq12f  4125  opelopabsb  4307  elrelimasn  5049  fvelrnb  5628  fmptco  5748  fconstfvm  5804  f1oiso  5897  canth  5899  mpoeq123  6006  elovmporab  6148  elovmporab1w  6149  dfoprab4f  6281  fmpox  6288  nnmword  6606  elfi  7075  ltmpig  7454  mul0eqap  8745  qreccl  9765  0fz1  10169  zmodid2  10499  divgcdcoprm0  12456  cnptoprest  14744  txrest  14781  cbvrald  15761