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  931  rbaibd  932  syl3an9b  1347  sbcomxyyz  2028  eqeq12  2247  eleq12  2299  sbhypf  2866  ceqsrex2v  2951  sseq12  3265  rexprg  3743  rextpg  3745  breq12  4116  opelopabg  4388  brabg  4389  opelopabgf  4390  opelopab2  4391  ralxpf  4903  rexxpf  4904  feq23  5496  f00  5561  fconstg  5566  f1oeq23  5607  f1o00  5653  f1oiso  6001  riota1a  6026  cbvmpox  6133  caovord  6228  caovord3  6230  rbropapd  6475  suppeqfsuppbi  7250  isacnm  7512  genpelvl  7829  genpelvu  7830  nn0ind-raph  9698  elpq  9984  xnn0xadd0  10203  elfz  10351  elfzp12  10437  wrd2ind  11419  shftfibg  11509  shftfib  11512  absdvdsb  12499  dvdsabsb  12500  dvdsabseq  12537  islmod  14456  znidom  14822  tgss2  14961  lmbr  15095  xmetec  15319  2lgslem1a  15978  edgiedgbg  16077