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  4135  opelopabg  4410  brabg  4411  opelopabgf  4412  opelopab2  4413  ralxpf  4926  rexxpf  4927  feq23  5519  f00  5584  fconstg  5589  f1oeq23  5630  f1o00  5676  f1oiso  6032  riota1a  6059  cbvmpox  6166  caovord  6261  caovord3  6263  rbropapd  6513  suppeqfsuppbi  7295  isacnm  7559  genpelvl  7879  genpelvu  7880  nn0ind-raph  9767  elpq  10059  xnn0xadd0  10279  elfz  10427  elfzp12  10516  wrd2ind  11509  shftfibg  11599  shftfib  11602  absdvdsb  12592  dvdsabsb  12593  dvdsabseq  12630  islmod  14676  znidom  15041  tgss2  15229  lmbr  15363  xmetec  15587  2lgslem1a  16305  edgiedgbg  16404