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  899  dn1dc  955  bilukdc  1391  nf4dc  1663  sbal1  1995  abbi  2284  necon3abid  2379  necon3bid  2381  necon1abiidc  2400  r19.21t  2545  ceqsralt  2757  ceqsrexv  2860  ceqsrex2v  2862  elab2g  2877  elrabf  2884  eueq2dc  2903  euxfrdc  2916  eqreu  2922  reu8  2926  ru  2954  sbcralt  3031  sbcrext  3032  sbcne12g  3067  csbnestgf  3101  dfss4st  3360  rexsng  3624  ralprg  3634  rexprg  3635  difsn  3717  opthpr  3759  ralunsn  3784  dfiin2g  3906  iunxsng  3948  iunxsngf  3950  elpwuni  3962  pwnss  4145  exmid01  4184  opelopabt  4247  opelopabga  4248  brabga  4249  elsucg  4389  elsuc2g  4390  brab2a  4664  opeliunxp  4666  posng  4683  brab2ga  4686  csbdmg  4805  elrnmpt1  4862  elrnmptg  4863  poleloe  5010  elxp4  5098  elxp5  5099  cnvpom  5153  sbcfung  5222  dffun8  5226  fncnv  5264  fununi  5266  fnssresb  5310  fnimaeq0  5319  funcocnv2  5467  dffn5im  5542  funimass4  5547  fnsnfv  5555  dmfco  5564  fndmdif  5601  fndmin  5603  unpreima  5621  respreima  5624  fsn2  5670  fnressn  5682  fressnfv  5683  elunirn  5745  dff13  5747  fliftel  5772  isoini  5797  f1oiso  5805  acexmid  5852  eloprabga  5940  resoprab2  5950  ralrnmpo  5967  rexrnmpo  5968  ovid  5969  ov  5972  ovg  5991  ofrfval2  6077  fmpox  6179  1stconst  6200  2ndconst  6201  f1od2  6214  rbropapd  6221  brtpos2  6230  dfsmo2  6266  frecabcl  6378  brdifun  6540  eqerlem  6544  brecop  6603  erovlem  6605  mapsn  6668  mptelixpg  6712  map1  6790  xpsnen  6799  xpdom2  6809  xpf1o  6822  supubti  6976  infglbti  7002  ctssdccl  7088  nninfwlpoim  7154  ltpiord  7281  nlt1pig  7303  elinp  7436  ltdfpr  7468  genpassl  7486  genpassu  7487  1idprl  7552  1idpru  7553  gt0srpr  7710  mappsrprg  7766  map2psrprg  7767  peano2nnnn  7815  recidpirq  7820  axprecex  7842  xrlenlt  7984  addsubeq4  8134  renegcl  8180  lesub0  8398  recexaplem2  8570  conjmulap  8646  rerecclap  8647  creui  8876  peano2nn  8890  nndiv  8919  elznn0  9227  eqreznegel  9573  negelrp  9644  ltxr  9732  divelunit  9959  iccf1o  9961  elfz2  9972  elfzp1  10028  fzdifsuc  10037  fznn  10045  fzosplitsni  10191  fvinim0ffz  10197  frec2uzisod  10363  sq11i  10565  cjreb  10830  rexfiuz  10953  cau3lem  11078  pwm1geoserap1  11471  mertensabs  11500  divides  11751  dvdsabseq  11807  odd2np1  11832  oddm1even  11834  modremain  11888  infssuzex  11904  zsupssdc  11909  bezoutlemnewy  11951  bezoutlemstep  11952  bezoutlemmain  11953  bezoutlema  11954  bezoutlemb  11955  isprm2  12071  isprm4  12073  dvdsnprmd  12079  oddprmdvds  12306  4sqlem2  12341  issubm  12695  istopg  12791  basgen2  12875  isnei  12938  restdis  12978  iscn  12991  iscnp  12993  lmbr2  13008  lmbrf  13009  txcn  13069  cnmpt21  13085  blres  13228  isxms2  13246  metrest  13300  metcnp  13306  txmetcnp  13312  txmetcn  13313  cnblcld  13329  reopnap  13332  ioocosf1o  13569  bj-nn0sucALT  14013  apdiff  14080