Theorem sylan9bb 457

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)

Hypotheses

Ref	Expression
sylan9bb.1	|- ( ph -> ( ps <-> ch ) )
sylan9bb.2	|- ( th -> ( ch <-> ta ) )

Assertion

Ref	Expression
sylan9bb	|- ( ( ph /\ th ) -> ( ps <-> ta ) )

Proof of Theorem sylan9bb

Step	Hyp	Ref	Expression
1		sylan9bb.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	adantr 274	. 2 |- ( ( ph /\ th ) -> ( ps <-> ch ) )
3		sylan9bb.2	. . 3 |- ( th -> ( ch <-> ta ) )
4	3	adantl 275	. 2 |- ( ( ph /\ th ) -> ( ch <-> ta ) )
5	2, 4	bitrd 187	1 |- ( ( ph /\ th ) -> ( ps <-> ta ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylan9bbr  458  bi2anan9  595  baibd  908  rbaibd  909  syl3an9b  1288  sbcomxyyz  1945  eqeq12  2152  eleq12  2204  sbhypf  2735  ceqsrex2v  2817  sseq12  3122  rexprg  3575  rextpg  3577  breq12  3934  opelopabg  4190  brabg  4191  opelopab2  4192  ralxpf  4685  rexxpf  4686  feq23  5258  f00  5314  fconstg  5319  f1oeq23  5359  f1o00  5402  f1oiso  5727  riota1a  5749  cbvmpox  5849  caovord  5942  caovord3  5944  rbropapd  6139  genpelvl  7320  genpelvu  7321  nn0ind-raph  9168  xnn0xadd0  9650  elfz  9796  elfzp12  9879  shftfibg  10592  shftfib  10595  absdvdsb  11511  dvdsabsb  11512  dvdsabseq  11545  tgss2  12248  lmbr  12382  xmetec  12606