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  6517  suppeqfsuppbi  7300  isacnm  7565  genpelvl  7885  genpelvu  7886  nn0ind-raph  9774  elpq  10066  xnn0xadd0  10286  elfz  10434  elfzp12  10523  wrd2ind  11517  shftfibg  11607  shftfib  11610  absdvdsb  12601  dvdsabsb  12602  dvdsabseq  12639  islmod  14736  znidom  15101  tgss2  15305  lmbr  15439  xmetec  15663  2lgslem1a  16412  edgiedgbg  16511