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  912  dn1dc  969  bilukdc  1441  nf4dc  1718  sbal1  2055  abbi  2345  abbib  2349  necon3abid  2442  necon3bid  2444  necon1abiidc  2463  r19.21t  2608  ceqsralt  2831  ceqsrexv  2937  ceqsrex2v  2939  elab2g  2954  elrabf  2961  eueq2dc  2980  euxfrdc  2993  eqreu  2999  reu8  3003  ru  3031  sbcralt  3109  sbcrext  3110  sbcne12g  3146  csbnestgf  3181  dfss4st  3442  rexsng  3714  ralprg  3724  rexprg  3725  difsn  3815  opthpr  3860  ralunsn  3886  dfiin2g  4008  iunxsng  4051  iunxsngf  4053  elpwuni  4065  pwnss  4255  exmid01  4294  opelopabt  4362  opelopabga  4363  brabga  4364  opelopabgf  4370  elsucg  4507  elsuc2g  4508  brab2a  4785  opeliunxp  4787  posng  4804  brab2ga  4807  csbdmg  4931  elrnmpt1  4989  elrnmptg  4990  eliniseg2  5123  poleloe  5143  elxp4  5231  elxp5  5232  cnvpom  5286  sbcfung  5357  dffun8  5361  fncnv  5403  fununi  5405  fnssresb  5451  fnimaeq0  5461  funcocnv2  5617  dffn5im  5700  funimass4  5705  fnsnfv  5714  dmfco  5723  fndmdif  5761  fndmin  5763  unpreima  5780  respreima  5783  fsn2  5829  fnressn  5848  fressnfv  5849  elunirn  5917  dff13  5919  fliftel  5944  isoini  5969  f1oiso  5977  riotaeqimp  6006  acexmid  6027  fnbrovb  6073  eloprabga  6118  resoprab2  6128  ralrnmpo  6146  rexrnmpo  6147  ovid  6148  ov  6151  ovg  6171  ofrfval2  6261  fmpox  6374  1stconst  6395  2ndconst  6396  f1od2  6409  rbropapd  6451  brtpos2  6460  dfsmo2  6496  frecabcl  6608  brdifun  6772  eqerlem  6776  brecop  6837  erovlem  6839  mapsn  6902  mptelixpg  6946  map1  7030  xpsnen  7048  xpdom2  7058  xpf1o  7073  supubti  7241  infglbti  7267  ctssdccl  7353  nninfwlpoim  7421  nninfinfwlpo  7422  netap  7516  2omotaplemap  7519  ltpiord  7582  nlt1pig  7604  elinp  7737  ltdfpr  7769  genpassl  7787  genpassu  7788  1idprl  7853  1idpru  7854  gt0srpr  8011  mappsrprg  8067  map2psrprg  8068  peano2nnnn  8116  recidpirq  8121  axprecex  8143  xrlenlt  8286  addsubeq4  8436  renegcl  8482  lesub0  8701  recexaplem2  8874  conjmulap  8951  rerecclap  8952  creui  9182  peano2nn  9197  nndiv  9226  elznn0  9538  eqreznegel  9892  negelrp  9966  ltxr  10054  divelunit  10281  iccf1o  10284  elfz2  10295  elfzp1  10352  fzdifsuc  10361  fznn  10369  nelfzo  10432  fzosplitsni  10527  fvinim0ffz  10533  infssuzex  10539  zsupssdc  10544  frec2uzisod  10715  sq11i  10937  wrdval  11165  csbwrdg  11192  swrdnd  11289  wrd2ind  11353  cjreb  11489  rexfiuz  11612  cau3lem  11737  pwm1geoserap1  12132  mertensabs  12161  divides  12413  dvdsabseq  12471  odd2np1  12497  oddm1even  12499  modremain  12553  bezoutlemnewy  12630  bezoutlemstep  12631  bezoutlemmain  12632  bezoutlema  12633  bezoutlemb  12634  isprm2  12752  isprm4  12754  dvdsnprmd  12760  oddprmdvds  12990  4sqlem2  13025  4sqlem12  13038  xpsfrnel2  13492  issubm  13618  grplmulf1o  13720  grplactcnv  13748  issubg  13823  elnmz  13858  isghm  13893  ghmeqker  13921  srg1zr  14064  iscrng2  14092  issubrng  14277  aprval  14361  zndvds  14728  znleval  14732  psrbag  14748  istopg  14793  basgen2  14875  isnei  14938  restdis  14978  iscn  14991  iscnp  14993  lmbr2  15008  lmbrf  15009  txcn  15069  cnmpt21  15085  blres  15228  isxms2  15246  metrest  15300  metcnp  15306  txmetcnp  15312  txmetcn  15313  cnblcld  15329  reopnap  15340  ioocosf1o  15648  mpodvdsmulf1o  15787  gausslemma2dlem0i  15859  gausslemma2dlem1a  15860  lgseisenlem2  15873  lgsquadlem1  15879  lgsquadlem2  15880  2lgslem1a  15890  isuhgrm  15995  isushgrm  15996  isupgren  16019  isumgren  16029  isuspgren  16081  isusgren  16082  uhgr0v0e  16158  vtxdg0v  16218  iswlk  16247  wlk1walkdom  16283  istrl  16309  clwwlkn1  16342  clwwlkn2  16345  clwwlknonel  16356  clwwlknun  16365  iseupth  16371  eupthres  16381  eupth2lem1  16382  eupth2lemsfi  16402  bj-nn0sucALT  16677  apdiff  16763