Theorem sylan9bb 418

Description: Nested syllogism inference conjoining dissimilar antecedents.

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

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  sylan9bbr 419  bi2anan9 478  syl3an9b 634  sbcom 916  sbcom2 992  cleq12 1113  eleq12 1151  vsbcint 1438  sseq12 1523  breq12 2067  opabsb 2114  opelopabg 2115  f00 2773  fconstg 2775  f1o00 2823  isofrlem 2939  f1oiso 2942  f1oweOLD 2944  caoprcom 3067  caoprord 3070  caoprord3 3072  oaordex 3160  oaass 3163  pw2en 3348  mapdom2 3389  unfilem1 3438  carduni 3664  axrepndlem2 3739  distrlem4pr 3924  lt2sq 4414  nn0ltp1let 4556  zltp1let 4597  nn0ind 4612  seqsuclem 4669  ruclem12 4896  znnen 4930  jplem1 5701  chrelat 5757

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org