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  950  bilukdc  1386  nf4dc  1658  sbal1  1990  abbi  2280  necon3abid  2375  necon3bid  2377  necon1abiidc  2396  r19.21t  2541  ceqsralt  2753  ceqsrexv  2856  ceqsrex2v  2858  elab2g  2873  elrabf  2880  eueq2dc  2899  euxfrdc  2912  eqreu  2918  reu8  2922  ru  2950  sbcralt  3027  sbcrext  3028  sbcne12g  3063  csbnestgf  3097  dfss4st  3355  rexsng  3617  ralprg  3627  rexprg  3628  difsn  3710  opthpr  3752  ralunsn  3777  dfiin2g  3899  iunxsng  3941  iunxsngf  3943  elpwuni  3955  pwnss  4138  exmid01  4177  opelopabt  4240  opelopabga  4241  brabga  4242  elsucg  4382  elsuc2g  4383  brab2a  4657  opeliunxp  4659  posng  4676  brab2ga  4679  csbdmg  4798  elrnmpt1  4855  elrnmptg  4856  poleloe  5003  elxp4  5091  elxp5  5092  cnvpom  5146  sbcfung  5212  dffun8  5216  fncnv  5254  fununi  5256  fnssresb  5300  fnimaeq0  5309  funcocnv2  5457  dffn5im  5532  funimass4  5537  fnsnfv  5545  dmfco  5554  fndmdif  5590  fndmin  5592  unpreima  5610  respreima  5613  fsn2  5659  fnressn  5671  fressnfv  5672  elunirn  5734  dff13  5736  fliftel  5761  isoini  5786  f1oiso  5794  acexmid  5841  eloprabga  5929  resoprab2  5939  ralrnmpo  5956  rexrnmpo  5957  ovid  5958  ov  5961  ovg  5980  ofrfval2  6066  fmpox  6168  1stconst  6189  2ndconst  6190  f1od2  6203  rbropapd  6210  brtpos2  6219  dfsmo2  6255  frecabcl  6367  brdifun  6528  eqerlem  6532  brecop  6591  erovlem  6593  mapsn  6656  mptelixpg  6700  map1  6778  xpsnen  6787  xpdom2  6797  xpf1o  6810  supubti  6964  infglbti  6990  ctssdccl  7076  ltpiord  7260  nlt1pig  7282  elinp  7415  ltdfpr  7447  genpassl  7465  genpassu  7466  1idprl  7531  1idpru  7532  gt0srpr  7689  mappsrprg  7745  map2psrprg  7746  peano2nnnn  7794  recidpirq  7799  axprecex  7821  xrlenlt  7963  addsubeq4  8113  renegcl  8159  lesub0  8377  recexaplem2  8549  conjmulap  8625  rerecclap  8626  creui  8855  peano2nn  8869  nndiv  8898  elznn0  9206  eqreznegel  9552  negelrp  9623  ltxr  9711  divelunit  9938  iccf1o  9940  elfz2  9951  elfzp1  10007  fzdifsuc  10016  fznn  10024  fzosplitsni  10170  fvinim0ffz  10176  frec2uzisod  10342  sq11i  10544  cjreb  10808  rexfiuz  10931  cau3lem  11056  pwm1geoserap1  11449  mertensabs  11478  divides  11729  dvdsabseq  11785  odd2np1  11810  oddm1even  11812  modremain  11866  infssuzex  11882  zsupssdc  11887  bezoutlemnewy  11929  bezoutlemstep  11930  bezoutlemmain  11931  bezoutlema  11932  bezoutlemb  11933  isprm2  12049  isprm4  12051  dvdsnprmd  12057  oddprmdvds  12284  4sqlem2  12319  istopg  12637  basgen2  12721  isnei  12784  restdis  12824  iscn  12837  iscnp  12839  lmbr2  12854  lmbrf  12855  txcn  12915  cnmpt21  12931  blres  13074  isxms2  13092  metrest  13146  metcnp  13152  txmetcnp  13158  txmetcn  13159  cnblcld  13175  reopnap  13178  ioocosf1o  13415  bj-nn0sucALT  13860  apdiff  13927