Theorem syl5bb 191

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
syl5bb	|- ( ch -> ( ph <-> th ) )

Proof of Theorem syl5bb

Step	Hyp	Ref	Expression
1		syl5bb.1	. . 3 |- ( ph <-> ps )
2	1	a1i 9	. 2 |- ( ch -> ( ph <-> ps ) )
3		syl5bb.2	. 2 |- ( ch -> ( ps <-> th ) )
4	2, 3	bitrd 187	1 |- ( ch -> ( ph <-> th ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bitr2id  192  bitr3id  193  3bitr4g  222  imim21b  251  pm5.17dc  894  dn1dc  949  bilukdc  1385  nf4dc  1657  sbal1  1989  abbi  2278  necon3abid  2373  necon3bid  2375  necon1abiidc  2394  r19.21t  2539  ceqsralt  2748  ceqsrexv  2851  ceqsrex2v  2853  elab2g  2868  elrabf  2875  eueq2dc  2894  euxfrdc  2907  eqreu  2913  reu8  2917  ru  2945  sbcralt  3022  sbcrext  3023  sbcne12g  3058  csbnestgf  3092  dfss4st  3350  rexsng  3611  ralprg  3621  rexprg  3622  difsn  3704  opthpr  3746  ralunsn  3771  dfiin2g  3893  iunxsng  3935  iunxsngf  3937  elpwuni  3949  pwnss  4132  exmid01  4171  opelopabt  4234  opelopabga  4235  brabga  4236  elsucg  4376  elsuc2g  4377  brab2a  4651  opeliunxp  4653  posng  4670  brab2ga  4673  csbdmg  4792  elrnmpt1  4849  elrnmptg  4850  poleloe  4997  elxp4  5085  elxp5  5086  cnvpom  5140  sbcfung  5206  dffun8  5210  fncnv  5248  fununi  5250  fnssresb  5294  fnimaeq0  5303  funcocnv2  5451  dffn5im  5526  funimass4  5531  fnsnfv  5539  dmfco  5548  fndmdif  5584  fndmin  5586  unpreima  5604  respreima  5607  fsn2  5653  fnressn  5665  fressnfv  5666  elunirn  5728  dff13  5730  fliftel  5755  isoini  5780  f1oiso  5788  acexmid  5835  eloprabga  5920  resoprab2  5930  ralrnmpo  5947  rexrnmpo  5948  ovid  5949  ov  5952  ovg  5971  ofrfval2  6060  fmpox  6160  1stconst  6180  2ndconst  6181  f1od2  6194  rbropapd  6201  brtpos2  6210  dfsmo2  6246  frecabcl  6358  brdifun  6519  eqerlem  6523  brecop  6582  erovlem  6584  mapsn  6647  mptelixpg  6691  map1  6769  xpsnen  6778  xpdom2  6788  xpf1o  6801  supubti  6955  infglbti  6981  ctssdccl  7067  ltpiord  7251  nlt1pig  7273  elinp  7406  ltdfpr  7438  genpassl  7456  genpassu  7457  1idprl  7522  1idpru  7523  gt0srpr  7680  mappsrprg  7736  map2psrprg  7737  peano2nnnn  7785  recidpirq  7790  axprecex  7812  xrlenlt  7954  addsubeq4  8104  renegcl  8150  lesub0  8368  recexaplem2  8540  conjmulap  8616  rerecclap  8617  creui  8846  peano2nn  8860  nndiv  8889  elznn0  9197  eqreznegel  9543  negelrp  9614  ltxr  9702  divelunit  9929  iccf1o  9931  elfz2  9942  elfzp1  9997  fzdifsuc  10006  fznn  10014  fzosplitsni  10160  fvinim0ffz  10166  frec2uzisod  10332  sq11i  10534  cjreb  10794  rexfiuz  10917  cau3lem  11042  pwm1geoserap1  11435  mertensabs  11464  divides  11715  dvdsabseq  11770  odd2np1  11795  oddm1even  11797  modremain  11851  infssuzex  11867  zsupssdc  11872  bezoutlemnewy  11914  bezoutlemstep  11915  bezoutlemmain  11916  bezoutlema  11917  bezoutlemb  11918  isprm2  12028  isprm4  12030  dvdsnprmd  12036  oddprmdvds  12261  istopg  12538  basgen2  12622  isnei  12685  restdis  12725  iscn  12738  iscnp  12740  lmbr2  12755  lmbrf  12756  txcn  12816  cnmpt21  12832  blres  12975  isxms2  12993  metrest  13047  metcnp  13053  txmetcnp  13059  txmetcn  13060  cnblcld  13076  reopnap  13079  ioocosf1o  13316  bj-nn0sucALT  13695  apdiff  13761