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  10481  fvinim0ffz  10487  infssuzex  10493  zsupssdc  10498  frec2uzisod  10669  sq11i  10891  wrdval  11116  csbwrdg  11143  swrdnd  11240  wrd2ind  11304  cjreb  11427  rexfiuz  11550  cau3lem  11675  pwm1geoserap1  12070  mertensabs  12099  divides  12351  dvdsabseq  12409  odd2np1  12435  oddm1even  12437  modremain  12491  bezoutlemnewy  12568  bezoutlemstep  12569  bezoutlemmain  12570  bezoutlema  12571  bezoutlemb  12572  isprm2  12690  isprm4  12692  dvdsnprmd  12698  oddprmdvds  12928  4sqlem2  12963  4sqlem12  12976  xpsfrnel2  13430  issubm  13556  grplmulf1o  13658  grplactcnv  13686  issubg  13761  elnmz  13796  isghm  13831  ghmeqker  13859  srg1zr  14002  iscrng2  14030  issubrng  14215  aprval  14298  zndvds  14665  znleval  14669  psrbag  14685  istopg  14725  basgen2  14807  isnei  14870  restdis  14910  iscn  14923  iscnp  14925  lmbr2  14940  lmbrf  14941  txcn  15001  cnmpt21  15017  blres  15160  isxms2  15178  metrest  15232  metcnp  15238  txmetcnp  15244  txmetcn  15245  cnblcld  15261  reopnap  15272  ioocosf1o  15580  mpodvdsmulf1o  15716  gausslemma2dlem0i  15788  gausslemma2dlem1a  15789  lgseisenlem2  15802  lgsquadlem1  15808  lgsquadlem2  15809  2lgslem1a  15819  isuhgrm  15924  isushgrm  15925  isupgren  15948  isumgren  15958  isuspgren  16010  isusgren  16011  uhgr0v0e  16087  vtxdg0v  16147  iswlk  16176  wlk1walkdom  16212  istrl  16238  clwwlkn1  16271  clwwlkn2  16274  clwwlknonel  16285  clwwlknun  16294  iseupth  16300  eupthres  16310  eupth2lem1  16311  bj-nn0sucALT  16576  apdiff  16655