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  925  rbaibd  926  syl3an9b  1323  sbcomxyyz  2000  eqeq12  2218  eleq12  2270  sbhypf  2822  ceqsrex2v  2905  sseq12  3218  rexprg  3685  rextpg  3687  breq12  4049  opelopabg  4314  brabg  4315  opelopabgf  4316  opelopab2  4317  ralxpf  4824  rexxpf  4825  feq23  5411  f00  5467  fconstg  5472  f1oeq23  5513  f1o00  5557  f1oiso  5895  riota1a  5919  cbvmpox  6023  caovord  6118  caovord3  6120  rbropapd  6328  isacnm  7315  genpelvl  7625  genpelvu  7626  nn0ind-raph  9490  elpq  9770  xnn0xadd0  9989  elfz  10136  elfzp12  10221  shftfibg  11131  shftfib  11134  absdvdsb  12120  dvdsabsb  12121  dvdsabseq  12158  islmod  14053  znidom  14419  tgss2  14551  lmbr  14685  xmetec  14909  2lgslem1a  15565