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  968  mpteq12f  4164  opelopabsb  4348  elrelimasn  5094  fvelrnb  5681  fmptco  5801  fconstfvm  5857  f1oiso  5950  canth  5952  mpoeq123  6063  elovmporab  6205  elovmporab1w  6206  dfoprab4f  6339  fmpox  6346  nnmword  6664  elfi  7138  ltmpig  7526  mul0eqap  8817  qreccl  9837  0fz1  10241  zmodid2  10574  divgcdcoprm0  12623  cnptoprest  14913  txrest  14950  uhgreq12g  15876  cbvrald  16152