Theorem sylan9bb 458

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylan9bbr  459  bi2anan9  596  baibd  909  rbaibd  910  syl3an9b  1289  sbcomxyyz  1949  eqeq12  2167  eleq12  2219  sbhypf  2758  ceqsrex2v  2841  sseq12  3149  rexprg  3607  rextpg  3609  breq12  3966  opelopabg  4223  brabg  4224  opelopab2  4225  ralxpf  4725  rexxpf  4726  feq23  5298  f00  5354  fconstg  5359  f1oeq23  5399  f1o00  5442  f1oiso  5767  riota1a  5789  cbvmpox  5889  caovord  5982  caovord3  5984  rbropapd  6179  genpelvl  7411  genpelvu  7412  nn0ind-raph  9260  elpq  9535  xnn0xadd0  9749  elfz  9896  elfzp12  9979  shftfibg  10697  shftfib  10700  absdvdsb  11678  dvdsabsb  11679  dvdsabseq  11712  tgss2  12426  lmbr  12560  xmetec  12784