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  2905  ceqsrex2v  2975  sseq12  3295  rexprg  3777  rextpg  3779  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  sfintfin  4533  breq12  4645  opelopabg  4706  brabg  4707  opelopab2  4708  ralxpf  4828  feq23  5214  f00  5250  fconstg  5252  f1oeq23  5285  f1o00  5318  f1oiso  5500  caovord  5630  caovord3  5632  cbvmpt2x  5679  ovmpt2x  5713  composefn  5819  fnfullfun  5859  elce  6176  ce2  6193