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  4050  opelopabg  4315  brabg  4316  opelopabgf  4317  opelopab2  4318  ralxpf  4825  rexxpf  4826  feq23  5413  f00  5469  fconstg  5474  f1oeq23  5515  f1o00  5559  f1oiso  5897  riota1a  5921  cbvmpox  6025  caovord  6120  caovord3  6122  rbropapd  6330  isacnm  7317  genpelvl  7627  genpelvu  7628  nn0ind-raph  9492  elpq  9772  xnn0xadd0  9991  elfz  10138  elfzp12  10223  shftfibg  11164  shftfib  11167  absdvdsb  12153  dvdsabsb  12154  dvdsabseq  12191  islmod  14086  znidom  14452  tgss2  14584  lmbr  14718  xmetec  14942  2lgslem1a  15598  edgiedgbg  15692