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  1977  abbi  2253  necon3abid  2347  necon3bid  2349  necon1abiidc  2368  r19.21t  2507  ceqsralt  2713  ceqsrexv  2815  ceqsrex2v  2817  elab2g  2831  elrabf  2838  eueq2dc  2857  euxfrdc  2870  eqreu  2876  reu8  2880  ru  2908  sbcralt  2985  sbcrext  2986  sbcne12g  3020  csbnestgf  3052  dfss4st  3309  rexsng  3565  ralprg  3574  rexprg  3575  difsn  3657  opthpr  3699  ralunsn  3724  dfiin2g  3846  iunxsng  3888  iunxsngf  3890  elpwuni  3902  pwnss  4083  exmid01  4121  opelopabt  4184  opelopabga  4185  brabga  4186  elsucg  4326  elsuc2g  4327  brab2a  4592  opeliunxp  4594  posng  4611  brab2ga  4614  csbdmg  4733  elrnmpt1  4790  elrnmptg  4791  poleloe  4938  elxp4  5026  elxp5  5027  cnvpom  5081  sbcfung  5147  dffun8  5151  fncnv  5189  fununi  5191  fnssresb  5235  fnimaeq0  5244  funcocnv2  5392  dffn5im  5467  funimass4  5472  fnsnfv  5480  dmfco  5489  fndmdif  5525  fndmin  5527  unpreima  5545  respreima  5548  fsn2  5594  fnressn  5606  fressnfv  5607  elunirn  5667  dff13  5669  fliftel  5694  isoini  5719  f1oiso  5727  acexmid  5773  eloprabga  5858  resoprab2  5868  ralrnmpo  5885  rexrnmpo  5886  ovid  5887  ov  5890  ovg  5909  ofrfval2  5998  fmpox  6098  1stconst  6118  2ndconst  6119  f1od2  6132  rbropapd  6139  brtpos2  6148  dfsmo2  6184  frecabcl  6296  brdifun  6456  eqerlem  6460  brecop  6519  erovlem  6521  mapsn  6584  mptelixpg  6628  map1  6706  xpsnen  6715  xpdom2  6725  xpf1o  6738  supubti  6886  infglbti  6912  ctssdccl  6996  ltpiord  7127  nlt1pig  7149  elinp  7282  ltdfpr  7314  genpassl  7332  genpassu  7333  1idprl  7398  1idpru  7399  gt0srpr  7556  mappsrprg  7612  map2psrprg  7613  peano2nnnn  7661  recidpirq  7666  axprecex  7688  xrlenlt  7829  addsubeq4  7977  renegcl  8023  lesub0  8241  recexaplem2  8413  conjmulap  8489  rerecclap  8490  creui  8718  peano2nn  8732  nndiv  8761  elznn0  9069  eqreznegel  9406  negelrp  9475  ltxr  9562  divelunit  9785  iccf1o  9787  elfz2  9797  elfzp1  9852  fzdifsuc  9861  fznn  9869  fzosplitsni  10012  fvinim0ffz  10018  frec2uzisod  10180  sq11i  10382  cjreb  10638  rexfiuz  10761  cau3lem  10886  pwm1geoserap1  11277  mertensabs  11306  divides  11495  dvdsabseq  11545  odd2np1  11570  oddm1even  11572  modremain  11626  infssuzex  11642  bezoutlemnewy  11684  bezoutlemstep  11685  bezoutlemmain  11686  bezoutlema  11687  bezoutlemb  11688  isprm2  11798  isprm4  11800  dvdsnprmd  11806  istopg  12166  basgen2  12250  isnei  12313  restdis  12353  iscn  12366  iscnp  12368  lmbr2  12383  lmbrf  12384  txcn  12444  cnmpt21  12460  blres  12603  isxms2  12621  metrest  12675  metcnp  12681  txmetcnp  12687  txmetcn  12688  cnblcld  12704  reopnap  12707  bj-indeq  13127  bj-nn0sucALT  13176