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  2025  eqeq12  2244  eleq12  2296  sbhypf  2853  ceqsrex2v  2938  sseq12  3252  rexprg  3721  rextpg  3723  breq12  4093  opelopabg  4362  brabg  4363  opelopabgf  4364  opelopab2  4365  ralxpf  4876  rexxpf  4877  feq23  5468  f00  5528  fconstg  5533  f1oeq23  5574  f1o00  5620  f1oiso  5967  riota1a  5992  cbvmpox  6099  caovord  6194  caovord3  6196  rbropapd  6408  isacnm  7418  genpelvl  7732  genpelvu  7733  nn0ind-raph  9597  elpq  9883  xnn0xadd0  10102  elfz  10249  elfzp12  10334  wrd2ind  11308  shftfibg  11398  shftfib  11401  absdvdsb  12388  dvdsabsb  12389  dvdsabseq  12426  islmod  14324  znidom  14690  tgss2  14822  lmbr  14956  xmetec  15180  2lgslem1a  15836  edgiedgbg  15935