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  9763  elpq  10049  xnn0xadd0  10269  elfz  10417  elfzp12  10506  wrd2ind  11495  shftfibg  11585  shftfib  11588  absdvdsb  12576  dvdsabsb  12577  dvdsabseq  12614  islmod  14627  znidom  14992  tgss2  15180  lmbr  15314  xmetec  15538  2lgslem1a  16207  edgiedgbg  16306