Theorem sylan9bb 459

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  460  bi2anan9  601  baibd  918  rbaibd  919  syl3an9b  1305  sbcomxyyz  1965  eqeq12  2183  eleq12  2235  sbhypf  2779  ceqsrex2v  2862  sseq12  3172  rexprg  3635  rextpg  3637  breq12  3994  opelopabg  4253  brabg  4254  opelopab2  4255  ralxpf  4757  rexxpf  4758  feq23  5333  f00  5389  fconstg  5394  f1oeq23  5434  f1o00  5477  f1oiso  5805  riota1a  5828  cbvmpox  5931  caovord  6024  caovord3  6026  rbropapd  6221  genpelvl  7474  genpelvu  7475  nn0ind-raph  9329  elpq  9607  xnn0xadd0  9824  elfz  9971  elfzp12  10055  shftfibg  10784  shftfib  10787  absdvdsb  11771  dvdsabsb  11772  dvdsabseq  11807  tgss2  12873  lmbr  13007  xmetec  13231