Theorem sylan9bb 466

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  467  bi2anan9  614  baibd  935  rbaibd  936  syl3an9b  1351  sbcomxyyz  2032  eqeq12  2251  eleq12  2303  sbhypf  2872  ceqsrex2v  2958  sseq12  3273  rexprg  3757  rextpg  3759  breq12  4130  opelopabg  4405  brabg  4406  opelopabgf  4407  opelopab2  4408  ralxpf  4921  rexxpf  4922  feq23  5514  f00  5579  fconstg  5584  f1oeq23  5625  f1o00  5671  f1oiso  6022  riota1a  6049  cbvmpox  6156  caovord  6251  caovord3  6253  rbropapd  6503  suppeqfsuppbi  7285  isacnm  7549  genpelvl  7869  genpelvu  7870  nn0ind-raph  9742  elpq  10028  xnn0xadd0  10248  elfz  10396  elfzp12  10484  wrd2ind  11473  shftfibg  11563  shftfib  11566  absdvdsb  12554  dvdsabsb  12555  dvdsabseq  12592  islmod  14600  znidom  14964  tgss2  15103  lmbr  15237  xmetec  15461  2lgslem1a  16121  edgiedgbg  16220