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  924  rbaibd  925  syl3an9b  1321  sbcomxyyz  1991  eqeq12  2209  eleq12  2261  sbhypf  2813  ceqsrex2v  2896  sseq12  3209  rexprg  3675  rextpg  3677  breq12  4039  opelopabg  4303  brabg  4304  opelopabgf  4305  opelopab2  4306  ralxpf  4813  rexxpf  4814  feq23  5396  f00  5452  fconstg  5457  f1oeq23  5498  f1o00  5542  f1oiso  5876  riota1a  5900  cbvmpox  6004  caovord  6099  caovord3  6101  rbropapd  6309  isacnm  7286  genpelvl  7596  genpelvu  7597  nn0ind-raph  9460  elpq  9740  xnn0xadd0  9959  elfz  10106  elfzp12  10191  shftfibg  11002  shftfib  11005  absdvdsb  11991  dvdsabsb  11992  dvdsabseq  12029  islmod  13923  znidom  14289  tgss2  14399  lmbr  14533  xmetec  14757  2lgslem1a  15413