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  2058  abbibcom  2348  abbib  2352  necon3abid  2453  necon3bid  2455  necon1abiidc  2474  r19.21t  2619  ceqsralt  2843  ceqsrexv  2950  ceqsrex2v  2952  elab2g  2967  elrabf  2974  eueq2dc  2993  euxfrdc  3006  eqreu  3012  reu8  3016  ru  3044  sbcralt  3122  sbcrext  3123  sbcne12g  3159  csbnestgf  3194  dfss4st  3458  rexsng  3735  ralprg  3745  rexprg  3746  difsn  3836  opthpr  3881  ralunsn  3907  dfiin2g  4029  iunxsng  4072  iunxsngf  4074  elpwuni  4086  pwnss  4277  exmid01  4316  opelopabt  4385  opelopabga  4386  brabga  4387  opelopabgf  4393  elsucg  4530  elsuc2g  4531  brab2a  4808  opeliunxp  4810  posng  4827  brab2ga  4830  csbdmg  4955  elrnmpt1  5013  elrnmptg  5014  eliniseg2  5147  poleloe  5167  elxp4  5255  elxp5  5256  cnvpom  5310  sbcfung  5381  dffun8  5385  fncnv  5427  fununi  5429  fnssresb  5475  fnimaeq0  5485  funcocnv2  5644  dffn5im  5727  funimass4  5732  fnsnfv  5741  dmfco  5750  fndmdif  5788  fndmin  5790  unpreima  5807  respreima  5810  fsn2  5856  fnressn  5875  fressnfv  5876  elunirn  5945  dff13  5947  fliftel  5972  isoini  5997  f1oiso  6005  riotaeqimp  6036  acexmid  6057  fnbrovb  6103  eloprabga  6148  resoprab2  6158  ralrnmpo  6176  rexrnmpo  6177  ovid  6178  ov  6181  ovg  6201  ofrfval2  6292  fmpox  6409  1stconst  6430  2ndconst  6431  f1od2  6444  rbropapd  6486  brtpos2  6495  dfsmo2  6531  frecabcl  6643  brdifun  6807  eqerlem  6811  brecop  6872  erovlem  6874  mapsnd  6936  mapsn  6938  mptelixpg  6982  map1  7067  xpsnen  7085  xpdom2  7095  xpf1o  7110  mapunen  7117  supubti  7303  infglbti  7329  ctssdccl  7415  nninfwlpoim  7483  nninfinfwlpo  7484  netap  7584  2omotaplemap  7587  ltpiord  7650  nlt1pig  7672  elinp  7805  ltdfpr  7837  genpassl  7855  genpassu  7856  1idprl  7921  1idpru  7922  gt0srpr  8079  mappsrprg  8135  map2psrprg  8136  peano2nnnn  8184  recidpirq  8189  axprecex  8211  xrlenlt  8354  addsubeq4  8504  renegcl  8550  lesub0  8770  recexaplem2  8943  conjmulap  9020  rerecclap  9021  creui  9251  peano2nn  9266  nndiv  9295  elznn0  9609  eqreznegel  9964  negelrp  10038  ltxr  10127  divelunit  10354  iccf1o  10357  elfz2  10368  elfzp1  10428  fzdifsuc  10437  fznn  10445  nelfzo  10508  fzosplitsni  10603  fvinim0ffz  10609  infssuzex  10615  zsupssdc  10622  frec2uzisod  10793  sq11i  11015  wrdval  11252  csbwrdg  11279  swrdnd  11376  wrd2ind  11440  cjreb  11576  rexfiuz  11699  cau3lem  11824  pwm1geoserap1  12219  mertensabs  12248  divides  12500  dvdsabseq  12558  odd2np1  12584  oddm1even  12586  modremain  12640  bezoutlemnewy  12717  bezoutlemstep  12718  bezoutlemmain  12719  bezoutlema  12720  bezoutlemb  12721  isprm2  12839  isprm4  12841  dvdsnprmd  12847  oddprmdvds  13077  4sqlem2  13112  4sqlem12  13125  xpsfrnel2  13610  issubm  13727  grplmulf1o  13829  grplactcnv  13857  issubg  13926  elnmz  13961  isghm  13996  ghmeqker  14024  rng1zrlem  14198  iscrng2  14258  issubrng  14445  aprval  14529  zndvds  14923  znleval  14927  psrbag  14943  istopg  14990  basgen2  15072  isnei  15135  restdis  15175  iscn  15188  iscnp  15190  lmbr2  15205  lmbrf  15206  txcn  15266  cnmpt21  15282  blres  15425  isxms2  15443  metrest  15497  metcnp  15503  txmetcnp  15509  txmetcn  15510  cnblcld  15526  reopnap  15537  ioocosf1o  15845  mpodvdsmulf1o  15984  gausslemma2dlem0i  16056  gausslemma2dlem1a  16057  lgseisenlem2  16070  lgsquadlem1  16076  lgsquadlem2  16077  2lgslem1a  16087  isuhgrm  16192  isushgrm  16193  isupgren  16216  isumgren  16226  isuspgren  16278  isusgren  16279  uhgr0v0e  16355  vtxdg0v  16415  iswlk  16444  wlk1walkdom  16480  istrl  16506  clwwlkn1  16539  clwwlkn2  16542  clwwlknonel  16553  clwwlknun  16562  iseupth  16568  eupthres  16578  eupth2lem1  16579  eupth2lemsfi  16599  bj-nn0sucALT  16874  apdiff  16958