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  606  baibd  925  rbaibd  926  syl3an9b  1323  sbcomxyyz  2001  eqeq12  2220  eleq12  2272  sbhypf  2827  ceqsrex2v  2912  sseq12  3226  rexprg  3695  rextpg  3697  breq12  4064  opelopabg  4332  brabg  4333  opelopabgf  4334  opelopab2  4335  ralxpf  4842  rexxpf  4843  feq23  5431  f00  5489  fconstg  5494  f1oeq23  5535  f1o00  5580  f1oiso  5918  riota1a  5942  cbvmpox  6046  caovord  6141  caovord3  6143  rbropapd  6351  isacnm  7346  genpelvl  7660  genpelvu  7661  nn0ind-raph  9525  elpq  9805  xnn0xadd0  10024  elfz  10171  elfzp12  10256  wrd2ind  11214  shftfibg  11246  shftfib  11249  absdvdsb  12235  dvdsabsb  12236  dvdsabseq  12273  islmod  14168  znidom  14534  tgss2  14666  lmbr  14800  xmetec  15024  2lgslem1a  15680  edgiedgbg  15776