Theorem sylan9bb 680

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

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  sylan9bbr  681  bi2anan9  843  baibd  875  rbaibd  876  syl3an9b  1250  nanbi12  1297  sbcom  2089  sbcom2  2114  ax11eq  2193  ax11el  2194  eqeq12  2365  eleq12  2415  sbhypf  2904  ceqsrex2v  2974  sseq12  3294  rexprg  3776  rextpg  3778  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  sfintfin  4532  breq12  4644  opelopabg  4705  brabg  4706  opelopab2  4707  ralxpf  4827  feq23  5213  f00  5249  fconstg  5251  f1oeq23  5284  f1o00  5317  f1oiso  5499  caovord  5629  caovord3  5631  cbvmpt2x  5678  ovmpt2x  5712  composefn  5818  fnfullfun  5858  elce  6175  ce2  6192