Theorem sylan9bb 462

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  463  bi2anan9  608  baibd  928  rbaibd  929  syl3an9b  1344  sbcomxyyz  2023  eqeq12  2242  eleq12  2294  sbhypf  2850  ceqsrex2v  2935  sseq12  3249  rexprg  3718  rextpg  3720  breq12  4088  opelopabg  4356  brabg  4357  opelopabgf  4358  opelopab2  4359  ralxpf  4868  rexxpf  4869  feq23  5459  f00  5517  fconstg  5522  f1oeq23  5563  f1o00  5608  f1oiso  5950  riota1a  5975  cbvmpox  6082  caovord  6177  caovord3  6179  rbropapd  6388  isacnm  7385  genpelvl  7699  genpelvu  7700  nn0ind-raph  9564  elpq  9844  xnn0xadd0  10063  elfz  10210  elfzp12  10295  wrd2ind  11255  shftfibg  11331  shftfib  11334  absdvdsb  12320  dvdsabsb  12321  dvdsabseq  12358  islmod  14255  znidom  14621  tgss2  14753  lmbr  14887  xmetec  15111  2lgslem1a  15767  edgiedgbg  15865