Theorem bitrid 192

Description: A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)

Hypotheses

Ref	Expression
bitrid.1	|- ( ph <-> ps )
bitrid.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
bitrid	|- ( ch -> ( ph <-> th ) )

Proof of Theorem bitrid

Step	Hyp	Ref	Expression
1		bitrid.1	. . 3 |- ( ph <-> ps )
2	1	a1i 9	. 2 |- ( ch -> ( ph <-> ps ) )
3		bitrid.2	. 2 |- ( ch -> ( ps <-> th ) )
4	2, 3	bitrd 188	1 |- ( ch -> ( ph <-> th ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bitr2id  193  bitr3id  194  3bitr4g  223  imim21b  253  pm5.17dc  911  dn1dc  968  bilukdc  1440  nf4dc  1718  sbal1  2055  abbi  2345  necon3abid  2441  necon3bid  2443  necon1abiidc  2462  r19.21t  2607  ceqsralt  2830  ceqsrexv  2936  ceqsrex2v  2938  elab2g  2953  elrabf  2960  eueq2dc  2979  euxfrdc  2992  eqreu  2998  reu8  3002  ru  3030  sbcralt  3108  sbcrext  3109  sbcne12g  3145  csbnestgf  3180  dfss4st  3440  rexsng  3710  ralprg  3720  rexprg  3721  difsn  3810  opthpr  3855  ralunsn  3881  dfiin2g  4003  iunxsng  4046  iunxsngf  4048  elpwuni  4060  pwnss  4249  exmid01  4288  opelopabt  4356  opelopabga  4357  brabga  4358  opelopabgf  4364  elsucg  4501  elsuc2g  4502  brab2a  4779  opeliunxp  4781  posng  4798  brab2ga  4801  csbdmg  4925  elrnmpt1  4983  elrnmptg  4984  eliniseg2  5116  poleloe  5136  elxp4  5224  elxp5  5225  cnvpom  5279  sbcfung  5350  dffun8  5354  fncnv  5396  fununi  5398  fnssresb  5444  fnimaeq0  5454  funcocnv2  5608  dffn5im  5691  funimass4  5696  fnsnfv  5705  dmfco  5714  fndmdif  5752  fndmin  5754  unpreima  5772  respreima  5775  fsn2  5821  fnressn  5839  fressnfv  5840  elunirn  5906  dff13  5908  fliftel  5933  isoini  5958  f1oiso  5966  riotaeqimp  5995  acexmid  6016  fnbrovb  6062  eloprabga  6107  resoprab2  6117  ralrnmpo  6135  rexrnmpo  6136  ovid  6137  ov  6140  ovg  6160  ofrfval2  6251  fmpox  6364  1stconst  6385  2ndconst  6386  f1od2  6399  rbropapd  6407  brtpos2  6416  dfsmo2  6452  frecabcl  6564  brdifun  6728  eqerlem  6732  brecop  6793  erovlem  6795  mapsn  6858  mptelixpg  6902  map1  6986  xpsnen  7004  xpdom2  7014  xpf1o  7029  supubti  7197  infglbti  7223  ctssdccl  7309  nninfwlpoim  7377  nninfinfwlpo  7378  netap  7472  2omotaplemap  7475  ltpiord  7538  nlt1pig  7560  elinp  7693  ltdfpr  7725  genpassl  7743  genpassu  7744  1idprl  7809  1idpru  7810  gt0srpr  7967  mappsrprg  8023  map2psrprg  8024  peano2nnnn  8072  recidpirq  8077  axprecex  8099  xrlenlt  8243  addsubeq4  8393  renegcl  8439  lesub0  8658  recexaplem2  8831  conjmulap  8908  rerecclap  8909  creui  9139  peano2nn  9154  nndiv  9183  elznn0  9493  eqreznegel  9847  negelrp  9921  ltxr  10009  divelunit  10236  iccf1o  10238  elfz2  10249  elfzp1  10306  fzdifsuc  10315  fznn  10323  nelfzo  10386  fzosplitsni  10480  fvinim0ffz  10486  infssuzex  10492  zsupssdc  10497  frec2uzisod  10668  sq11i  10890  wrdval  11115  csbwrdg  11142  swrdnd  11239  wrd2ind  11303  cjreb  11426  rexfiuz  11549  cau3lem  11674  pwm1geoserap1  12068  mertensabs  12097  divides  12349  dvdsabseq  12407  odd2np1  12433  oddm1even  12435  modremain  12489  bezoutlemnewy  12566  bezoutlemstep  12567  bezoutlemmain  12568  bezoutlema  12569  bezoutlemb  12570  isprm2  12688  isprm4  12690  dvdsnprmd  12696  oddprmdvds  12926  4sqlem2  12961  4sqlem12  12974  xpsfrnel2  13428  issubm  13554  grplmulf1o  13656  grplactcnv  13684  issubg  13759  elnmz  13794  isghm  13829  ghmeqker  13857  srg1zr  13999  iscrng2  14027  issubrng  14212  aprval  14295  zndvds  14662  znleval  14666  psrbag  14682  istopg  14722  basgen2  14804  isnei  14867  restdis  14907  iscn  14920  iscnp  14922  lmbr2  14937  lmbrf  14938  txcn  14998  cnmpt21  15014  blres  15157  isxms2  15175  metrest  15229  metcnp  15235  txmetcnp  15241  txmetcn  15242  cnblcld  15258  reopnap  15269  ioocosf1o  15577  mpodvdsmulf1o  15713  gausslemma2dlem0i  15785  gausslemma2dlem1a  15786  lgseisenlem2  15799  lgsquadlem1  15805  lgsquadlem2  15806  2lgslem1a  15816  isuhgrm  15921  isushgrm  15922  isupgren  15945  isumgren  15955  isuspgren  16007  isusgren  16008  uhgr0v0e  16084  vtxdg0v  16144  iswlk  16173  wlk1walkdom  16209  istrl  16235  clwwlkn1  16268  clwwlkn2  16271  clwwlknonel  16282  clwwlknun  16291  iseupth  16297  eupthres  16307  eupth2lem1  16308  bj-nn0sucALT  16573  apdiff  16652