Theorem sylan9bb 449

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 270	. 2 |- ( ( ph /\ th ) -> ( ps <-> ch ) )
3		sylan9bb.2	. . 3 |- ( th -> ( ch <-> ta ) )
4	3	adantl 271	. 2 |- ( ( ph /\ th ) -> ( ch <-> ta ) )
5	2, 4	bitrd 186	1 |- ( ( ph /\ th ) -> ( ps <-> ta ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sylan9bbr  450  bi2anan9  570  baibd  865  rbaibd  866  syl3an9b  1241  sbcomxyyz  1887  eqeq12  2093  eleq12  2143  sbhypf  2648  ceqsrex2v  2727  sseq12  3022  rexprg  3444  rextpg  3446  breq12  3790  opelopabg  4023  brabg  4024  opelopab2  4025  ralxpf  4500  rexxpf  4501  feq23  5053  f00  5101  fconstg  5103  f1oeq23  5140  f1o00  5181  f1oiso  5485  riota1a  5507  cbvmpt2x  5602  caovord  5692  caovord3  5694  genpelvl  6702  genpelvu  6703  nn0ind-raph  8464  elfz  9035  elfzp12  9116  shftfibg  9708  shftfib  9711  absdvdsb  10213  dvdsabsb  10214  dvdsabseq  10247