Theorem sylbb2 228

Description: A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.)

Hypotheses

Ref	Expression
sylbb2.1	|- ( ph <-> ps )
sylbb2.2	|- ( ch <-> ps )

Assertion

Ref	Expression
sylbb2	|- ( ph -> ch )

Proof of Theorem sylbb2

Step	Hyp	Ref	Expression
1		sylbb2.1	. 2 |- ( ph <-> ps )
2		sylbb2.2	. . 3 |- ( ch <-> ps )
3	2	biimpri 218	. 2 |- ( ps -> ch )
4	1, 3	sylbi 207	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  ftpg  6423  wfrlem5  7419  funsnfsupp  8299  fin23lem40  9173  s4f1o  13663  fsumsplitsnun  14484  fsumsplitsnunOLD  14486  lcmcllem  15309  mat1dimbas  20278  pmatcollpw3fi  20590  nbgrssvwo2  26261  wlkn0  26516  konigsberglem5  27118  eulerpartlemgs2  30442  bnj1476  30917  bnj1204  31080  dfon2lem3  31690  frrlem5  31784  bj-ccinftydisj  33100  nninfnub  33547  ispridl2  33837  rp-isfinite6  37864  fnresfnco  41206