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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylan9bbr  467  bi2anan9  614  baibd  935  rbaibd  936  syl3an9b  1351  sbcomxyyz  2032  eqeq12  2251  eleq12  2303  sbhypf  2872  ceqsrex2v  2958  sseq12  3273  rexprg  3761  rextpg  3763  breq12  4136  opelopabg  4412  brabg  4413  opelopabgf  4414  opelopab2  4415  ralxpf  4928  rexxpf  4929  feq23  5522  f00  5587  fconstg  5592  f1oeq23  5633  f1o00  5679  f1oiso  6035  riota1a  6062  cbvmpox  6169  caovord  6264  caovord3  6266  rbropapd  6518  isacnm  7565  genpelvl  7885  genpelvu  7886  nn0ind-raph  9773  elpq  10065  xnn0xadd0  10285  elfz  10433  elfzp12  10522  wrd2ind  11516  shftfibg  11606  shftfib  11609  absdvdsb  12600  dvdsabsb  12601  dvdsabseq  12638  islmod  14735  znidom  15100  tgss2  15322  lmbr  15456  xmetec  15680  2lgslem1a  16429  edgiedgbg  16528