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  5840  fressnfv  5841  elunirn  5907  dff13  5909  fliftel  5934  isoini  5959  f1oiso  5967  riotaeqimp  5996  acexmid  6017  fnbrovb  6063  eloprabga  6108  resoprab2  6118  ralrnmpo  6136  rexrnmpo  6137  ovid  6138  ov  6141  ovg  6161  ofrfval2  6252  fmpox  6365  1stconst  6386  2ndconst  6387  f1od2  6400  rbropapd  6408  brtpos2  6417  dfsmo2  6453  frecabcl  6565  brdifun  6729  eqerlem  6733  brecop  6794  erovlem  6796  mapsn  6859  mptelixpg  6903  map1  6987  xpsnen  7005  xpdom2  7015  xpf1o  7030  supubti  7198  infglbti  7224  ctssdccl  7310  nninfwlpoim  7378  nninfinfwlpo  7379  netap  7473  2omotaplemap  7476  ltpiord  7539  nlt1pig  7561  elinp  7694  ltdfpr  7726  genpassl  7744  genpassu  7745  1idprl  7810  1idpru  7811  gt0srpr  7968  mappsrprg  8024  map2psrprg  8025  peano2nnnn  8073  recidpirq  8078  axprecex  8100  xrlenlt  8244  addsubeq4  8394  renegcl  8440  lesub0  8659  recexaplem2  8832  conjmulap  8909  rerecclap  8910  creui  9140  peano2nn  9155  nndiv  9184  elznn0  9494  eqreznegel  9848  negelrp  9922  ltxr  10010  divelunit  10237  iccf1o  10239  elfz2  10250  elfzp1  10307  fzdifsuc  10316  fznn  10324  nelfzo  10387  fzosplitsni  10482  fvinim0ffz  10488  infssuzex  10494  zsupssdc  10499  frec2uzisod  10670  sq11i  10892  wrdval  11120  csbwrdg  11147  swrdnd  11244  wrd2ind  11308  cjreb  11444  rexfiuz  11567  cau3lem  11692  pwm1geoserap1  12087  mertensabs  12116  divides  12368  dvdsabseq  12426  odd2np1  12452  oddm1even  12454  modremain  12508  bezoutlemnewy  12585  bezoutlemstep  12586  bezoutlemmain  12587  bezoutlema  12588  bezoutlemb  12589  isprm2  12707  isprm4  12709  dvdsnprmd  12715  oddprmdvds  12945  4sqlem2  12980  4sqlem12  12993  xpsfrnel2  13447  issubm  13573  grplmulf1o  13675  grplactcnv  13703  issubg  13778  elnmz  13813  isghm  13848  ghmeqker  13876  srg1zr  14019  iscrng2  14047  issubrng  14232  aprval  14315  zndvds  14682  znleval  14686  psrbag  14702  istopg  14742  basgen2  14824  isnei  14887  restdis  14927  iscn  14940  iscnp  14942  lmbr2  14957  lmbrf  14958  txcn  15018  cnmpt21  15034  blres  15177  isxms2  15195  metrest  15249  metcnp  15255  txmetcnp  15261  txmetcn  15262  cnblcld  15278  reopnap  15289  ioocosf1o  15597  mpodvdsmulf1o  15733  gausslemma2dlem0i  15805  gausslemma2dlem1a  15806  lgseisenlem2  15819  lgsquadlem1  15825  lgsquadlem2  15826  2lgslem1a  15836  isuhgrm  15941  isushgrm  15942  isupgren  15965  isumgren  15975  isuspgren  16027  isusgren  16028  uhgr0v0e  16104  vtxdg0v  16164  iswlk  16193  wlk1walkdom  16229  istrl  16255  clwwlkn1  16288  clwwlkn2  16291  clwwlknonel  16302  clwwlknun  16311  iseupth  16317  eupthres  16327  eupth2lem1  16328  eupth2lemsfi  16348  bj-nn0sucALT  16624  apdiff  16703