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:  syl5rbb  192  syl5bbr  193  3bitr4g  222  imim21b  251  pm5.17dc  889  dn1dc  944  bilukdc  1374  nf4dc  1648  sbal1  1975  abbi  2251  necon3abid  2345  necon3bid  2347  necon1abiidc  2366  r19.21t  2505  ceqsralt  2708  ceqsrexv  2810  ceqsrex2v  2812  elab2g  2826  elrabf  2833  eueq2dc  2852  euxfrdc  2865  eqreu  2871  reu8  2875  ru  2903  sbcralt  2980  sbcrext  2981  sbcne12g  3015  csbnestgf  3047  dfss4st  3304  rexsng  3560  ralprg  3569  rexprg  3570  difsn  3652  opthpr  3694  ralunsn  3719  dfiin2g  3841  iunxsng  3883  iunxsngf  3885  elpwuni  3897  pwnss  4078  exmid01  4116  opelopabt  4179  opelopabga  4180  brabga  4181  elsucg  4321  elsuc2g  4322  brab2a  4587  opeliunxp  4589  posng  4606  brab2ga  4609  csbdmg  4728  elrnmpt1  4785  elrnmptg  4786  poleloe  4933  elxp4  5021  elxp5  5022  cnvpom  5076  sbcfung  5142  dffun8  5146  fncnv  5184  fununi  5186  fnssresb  5230  fnimaeq0  5239  funcocnv2  5385  dffn5im  5460  funimass4  5465  fnsnfv  5473  dmfco  5482  fndmdif  5518  fndmin  5520  unpreima  5538  respreima  5541  fsn2  5587  fnressn  5599  fressnfv  5600  elunirn  5660  dff13  5662  fliftel  5687  isoini  5712  f1oiso  5720  acexmid  5766  eloprabga  5851  resoprab2  5861  ralrnmpo  5878  rexrnmpo  5879  ovid  5880  ov  5883  ovg  5902  ofrfval2  5991  fmpox  6091  1stconst  6111  2ndconst  6112  f1od2  6125  rbropapd  6132  brtpos2  6141  dfsmo2  6177  frecabcl  6289  brdifun  6449  eqerlem  6453  brecop  6512  erovlem  6514  mapsn  6577  mptelixpg  6621  map1  6699  xpsnen  6708  xpdom2  6718  xpf1o  6731  supubti  6879  infglbti  6905  ctssdccl  6989  ltpiord  7120  nlt1pig  7142  elinp  7275  ltdfpr  7307  genpassl  7325  genpassu  7326  1idprl  7391  1idpru  7392  gt0srpr  7549  mappsrprg  7605  map2psrprg  7606  peano2nnnn  7654  recidpirq  7659  axprecex  7681  xrlenlt  7822  addsubeq4  7970  renegcl  8016  lesub0  8234  recexaplem2  8406  conjmulap  8482  rerecclap  8483  creui  8711  peano2nn  8725  nndiv  8754  elznn0  9062  eqreznegel  9399  negelrp  9468  ltxr  9555  divelunit  9778  iccf1o  9780  elfz2  9790  elfzp1  9845  fzdifsuc  9854  fznn  9862  fzosplitsni  10005  fvinim0ffz  10011  frec2uzisod  10173  sq11i  10375  cjreb  10631  rexfiuz  10754  cau3lem  10879  pwm1geoserap1  11270  mertensabs  11299  divides  11484  dvdsabseq  11534  odd2np1  11559  oddm1even  11561  modremain  11615  infssuzex  11631  bezoutlemnewy  11673  bezoutlemstep  11674  bezoutlemmain  11675  bezoutlema  11676  bezoutlemb  11677  isprm2  11787  isprm4  11789  dvdsnprmd  11795  istopg  12155  basgen2  12239  isnei  12302  restdis  12342  iscn  12355  iscnp  12357  lmbr2  12372  lmbrf  12373  txcn  12433  cnmpt21  12449  blres  12592  isxms2  12610  metrest  12664  metcnp  12670  txmetcnp  12676  txmetcn  12677  cnblcld  12693  reopnap  12696  bj-indeq  13116  bj-nn0sucALT  13165