Theorem sylan9bbr 451

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

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm5.75  904  mpteq12f  3866  opelopabsb  4023  elreimasng  4721  fvelrnb  5253  fmptco  5362  fconstfvm  5411  f1oiso  5496  mpt2eq123  5595  dfoprab4f  5850  fmpt2x  5857  nnmword  6157  ltmpig  6591  qreccl  8808  0fz1  9140  zmodid2  9434  divgcdcoprm0  10627  cbvrald  10749