Theorem sylan9bb 450

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sylan9bbr  451  bi2anan9  571  baibd  866  rbaibd  867  syl3an9b  1242  sbcomxyyz  1888  eqeq12  2094  eleq12  2144  sbhypf  2649  ceqsrex2v  2728  sseq12  3023  rexprg  3452  rextpg  3454  breq12  3798  opelopabg  4031  brabg  4032  opelopab2  4033  ralxpf  4510  rexxpf  4511  feq23  5064  f00  5112  fconstg  5114  f1oeq23  5151  f1o00  5192  f1oiso  5496  riota1a  5518  cbvmpt2x  5613  caovord  5703  caovord3  5705  genpelvl  6764  genpelvu  6765  nn0ind-raph  8545  elfz  9111  elfzp12  9192  shftfibg  9846  shftfib  9849  absdvdsb  10358  dvdsabsb  10359  dvdsabseq  10392