Theorem sylbb 209

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

Hypotheses

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

Assertion

Ref	Expression
sylbb	|- ( ph -> ch )

Proof of Theorem sylbb

Step	Hyp	Ref	Expression
1		sylbb.1	. 2 |- ( ph <-> ps )
2		sylbb.2	. . 3 |- ( ps <-> ch )
3	2	biimpi 206	. 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:  bitri  264  ssdifim  3862  disjxiun  4649  trint  4768  pocl  5042  wefrc  5108  frsn  5189  ssrel  5207  funiun  6412  funopsn  6413  fissuni  8271  inf3lem2  8526  rankvalb  8660  xrrebnd  11999  xaddf  12055  elfznelfzob  12574  fsuppmapnn0ub  12795  hashinfxadd  13174  hashfun  13224  clatl  17116  sgrp2nmndlem5  17416  mat1dimelbas  20277  cfinfil  21697  dyadmax  23366  ausgrusgri  26063  nbupgrres  26266  usgredgsscusgredg  26355  1egrvtxdg0  26407  wlkp1lem7  26576  wwlksnfi  26801  isch3  28098  nmopun  28873  esumnul  30110  dya2iocnrect  30343  bnj849  30995  bnj1279  31086  bj-0int  33055  onsucuni3  33215  wl-nfeqfb  33323  poimirlem27  33436  unitresl  33884  iunrelexp0  37994  frege129d  38055  clsk3nimkb  38338  gneispace  38432  eliuniin  39279  eliuniin2  39303  stoweidlem48  40265  fourierdlem42  40366  fourierdlem80  40403  oddprmALTV  41598  alimp-no-surprise  42527