Theorem syl5bb 190

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 186	1 |- ( ch -> ( ph <-> th ) )

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  syl5rbb  191  syl5bbr  192  3bitr4g  221  imim21b  250  pm5.17dc  843  dn1dc  901  bilukdc  1327  nf4dc  1600  sbal1  1919  abbi  2192  necon3abid  2284  necon3bid  2286  necon1abiidc  2305  r19.21t  2436  ceqsralt  2626  ceqsrexv  2725  ceqsrex2v  2727  elab2g  2740  elrabf  2747  eueq2dc  2765  euxfrdc  2778  eqreu  2784  reu8  2788  ru  2814  sbcralt  2890  sbcrext  2891  sbcne12g  2924  csbnestgf  2954  rexsng  3434  ralprg  3443  rexprg  3444  difsn  3523  opthpr  3564  ralunsn  3589  dfiin2g  3711  iunxsng  3753  elpwuni  3762  pwnss  3933  opelopabt  4017  opelopabga  4018  brabga  4019  elsucg  4159  elsuc2g  4160  brab2a  4411  opeliunxp  4413  posng  4430  brab2ga  4433  csbdmg  4547  elrnmpt1  4603  elrnmptg  4604  poleloe  4744  elxp4  4828  elxp5  4829  cnvpom  4880  sbcfung  4945  dffun8  4949  fncnv  4985  fununi  4987  fnssresb  5031  fnimaeq0  5040  funcocnv2  5171  dffn5im  5240  funimass4  5245  fnsnfv  5253  dmfco  5262  fndmdif  5293  fndmin  5295  unpreima  5313  respreima  5316  fsn2  5358  fnressn  5370  fressnfv  5371  elunirn  5426  dff13  5428  fliftel  5453  isoini  5477  f1oiso  5485  acexmid  5531  eloprabga  5611  resoprab2  5618  ralrnmpt2  5635  rexrnmpt2  5636  ovid  5637  ov  5640  ovg  5659  ofrfval2  5747  fmpt2x  5846  1stconst  5862  2ndconst  5863  f1od2  5876  isprmpt2  5881  brtpos2  5889  dfsmo2  5925  brdifun  6156  eqerlem  6160  brecop  6219  erovlem  6221  xpsnen  6318  xpdom2  6328  supubti  6412  infglbti  6438  ltpiord  6509  nlt1pig  6531  elinp  6664  ltdfpr  6696  genpassl  6714  genpassu  6715  1idprl  6780  1idpru  6781  gt0srpr  6925  peano2nnnn  7021  recidpirq  7026  axprecex  7046  xrlenlt  7177  addsubeq4  7323  renegcl  7369  lesub0  7583  recexaplem2  7742  conjmulap  7817  rerecclap  7818  creui  8037  peano2nn  8051  nndiv  8079  elznn0  8366  eqreznegel  8699  ltxr  8849  divelunit  9024  iccf1o  9026  elfz2  9036  elfzp1  9089  fzdifsuc  9098  fznn  9106  fzosplitsni  9244  fvinim0ffz  9250  frec2uzisod  9409  sq11i  9565  cjreb  9753  rexfiuz  9875  cau3lem  10000  divides  10197  dvdsabseq  10247  odd2np1  10272  oddm1even  10274  modremain  10329  infssuzex  10345  bezoutlemnewy  10385  bezoutlemstep  10386  bezoutlemmain  10387  bezoutlema  10388  bezoutlemb  10389  isprm2  10499  isprm4  10501  dvdsnprmd  10507  bj-indeq  10724  bj-nn0sucALT  10773