Theorem sylan9bb 462

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 276	. 2 |- ( ( ph /\ th ) -> ( ps <-> ch ) )
3		sylan9bb.2	. . 3 |- ( th -> ( ch <-> ta ) )
4	3	adantl 277	. 2 |- ( ( ph /\ th ) -> ( ch <-> ta ) )
5	2, 4	bitrd 188	1 |- ( ( ph /\ th ) -> ( 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:  sylan9bbr  463  bi2anan9  606  baibd  923  rbaibd  924  syl3an9b  1310  sbcomxyyz  1972  eqeq12  2190  eleq12  2242  sbhypf  2787  ceqsrex2v  2870  sseq12  3181  rexprg  3645  rextpg  3647  breq12  4009  opelopabg  4269  brabg  4270  opelopab2  4271  ralxpf  4774  rexxpf  4775  feq23  5352  f00  5408  fconstg  5413  f1oeq23  5453  f1o00  5497  f1oiso  5827  riota1a  5850  cbvmpox  5953  caovord  6046  caovord3  6048  rbropapd  6243  genpelvl  7511  genpelvu  7512  nn0ind-raph  9370  elpq  9648  xnn0xadd0  9867  elfz  10014  elfzp12  10099  shftfibg  10829  shftfib  10832  absdvdsb  11816  dvdsabsb  11817  dvdsabseq  11853  islmod  13381  tgss2  13582  lmbr  13716  xmetec  13940