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  2025  eqeq12  2244  eleq12  2296  sbhypf  2854  ceqsrex2v  2939  sseq12  3253  rexprg  3725  rextpg  3727  breq12  4098  opelopabg  4368  brabg  4369  opelopabgf  4370  opelopab2  4371  ralxpf  4882  rexxpf  4883  feq23  5475  f00  5537  fconstg  5542  f1oeq23  5583  f1o00  5629  f1oiso  5977  riota1a  6002  cbvmpox  6109  caovord  6204  caovord3  6206  rbropapd  6451  suppeqfsuppbi  7220  isacnm  7478  genpelvl  7792  genpelvu  7793  nn0ind-raph  9658  elpq  9944  xnn0xadd0  10163  elfz  10311  elfzp12  10396  wrd2ind  11370  shftfibg  11460  shftfib  11463  absdvdsb  12450  dvdsabsb  12451  dvdsabseq  12488  islmod  14387  znidom  14753  tgss2  14890  lmbr  15024  xmetec  15248  2lgslem1a  15907  edgiedgbg  16006