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  610  baibd  930  rbaibd  931  syl3an9b  1346  sbcomxyyz  2024  eqeq12  2243  eleq12  2295  sbhypf  2852  ceqsrex2v  2937  sseq12  3251  rexprg  3720  rextpg  3722  breq12  4092  opelopabg  4361  brabg  4362  opelopabgf  4363  opelopab2  4364  ralxpf  4875  rexxpf  4876  feq23  5467  f00  5528  fconstg  5533  f1oeq23  5574  f1o00  5620  f1oiso  5969  riota1a  5994  cbvmpox  6101  caovord  6196  caovord3  6198  rbropapd  6410  isacnm  7420  genpelvl  7734  genpelvu  7735  nn0ind-raph  9599  elpq  9885  xnn0xadd0  10104  elfz  10251  elfzp12  10336  wrd2ind  11310  shftfibg  11400  shftfib  11403  absdvdsb  12390  dvdsabsb  12391  dvdsabseq  12428  islmod  14326  znidom  14692  tgss2  14829  lmbr  14963  xmetec  15187  2lgslem1a  15843  edgiedgbg  15942