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  904  dn1dc  960  bilukdc  1396  nf4dc  1670  sbal1  2002  abbi  2291  necon3abid  2386  necon3bid  2388  necon1abiidc  2407  r19.21t  2552  ceqsralt  2766  ceqsrexv  2869  ceqsrex2v  2871  elab2g  2886  elrabf  2893  eueq2dc  2912  euxfrdc  2925  eqreu  2931  reu8  2935  ru  2963  sbcralt  3041  sbcrext  3042  sbcne12g  3077  csbnestgf  3111  dfss4st  3370  rexsng  3635  ralprg  3645  rexprg  3646  difsn  3731  opthpr  3774  ralunsn  3799  dfiin2g  3921  iunxsng  3964  iunxsngf  3966  elpwuni  3978  pwnss  4161  exmid01  4200  opelopabt  4264  opelopabga  4265  brabga  4266  elsucg  4406  elsuc2g  4407  brab2a  4681  opeliunxp  4683  posng  4700  brab2ga  4703  csbdmg  4823  elrnmpt1  4880  elrnmptg  4881  eliniseg2  5010  poleloe  5030  elxp4  5118  elxp5  5119  cnvpom  5173  sbcfung  5242  dffun8  5246  fncnv  5284  fununi  5286  fnssresb  5330  fnimaeq0  5339  funcocnv2  5488  dffn5im  5563  funimass4  5568  fnsnfv  5577  dmfco  5586  fndmdif  5623  fndmin  5625  unpreima  5643  respreima  5646  fsn2  5692  fnressn  5704  fressnfv  5705  elunirn  5769  dff13  5771  fliftel  5796  isoini  5821  f1oiso  5829  acexmid  5876  eloprabga  5964  resoprab2  5974  ralrnmpo  5991  rexrnmpo  5992  ovid  5993  ov  5996  ovg  6015  ofrfval2  6101  fmpox  6203  1stconst  6224  2ndconst  6225  f1od2  6238  rbropapd  6245  brtpos2  6254  dfsmo2  6290  frecabcl  6402  brdifun  6564  eqerlem  6568  brecop  6627  erovlem  6629  mapsn  6692  mptelixpg  6736  map1  6814  xpsnen  6823  xpdom2  6833  xpf1o  6846  supubti  7000  infglbti  7026  ctssdccl  7112  nninfwlpoim  7178  netap  7255  2omotaplemap  7258  ltpiord  7320  nlt1pig  7342  elinp  7475  ltdfpr  7507  genpassl  7525  genpassu  7526  1idprl  7591  1idpru  7592  gt0srpr  7749  mappsrprg  7805  map2psrprg  7806  peano2nnnn  7854  recidpirq  7859  axprecex  7881  xrlenlt  8024  addsubeq4  8174  renegcl  8220  lesub0  8438  recexaplem2  8611  conjmulap  8688  rerecclap  8689  creui  8919  peano2nn  8933  nndiv  8962  elznn0  9270  eqreznegel  9616  negelrp  9689  ltxr  9777  divelunit  10004  iccf1o  10006  elfz2  10017  elfzp1  10074  fzdifsuc  10083  fznn  10091  fzosplitsni  10237  fvinim0ffz  10243  frec2uzisod  10409  sq11i  10612  cjreb  10877  rexfiuz  11000  cau3lem  11125  pwm1geoserap1  11518  mertensabs  11547  divides  11798  dvdsabseq  11855  odd2np1  11880  oddm1even  11882  modremain  11936  infssuzex  11952  zsupssdc  11957  bezoutlemnewy  11999  bezoutlemstep  12000  bezoutlemmain  12001  bezoutlema  12002  bezoutlemb  12003  isprm2  12119  isprm4  12121  dvdsnprmd  12127  oddprmdvds  12354  4sqlem2  12389  xpsfrnel2  12770  issubm  12868  grplmulf1o  12949  grplactcnv  12977  issubg  13038  elnmz  13073  srg1zr  13175  iscrng2  13203  aprval  13377  istopg  13538  basgen2  13620  isnei  13683  restdis  13723  iscn  13736  iscnp  13738  lmbr2  13753  lmbrf  13754  txcn  13814  cnmpt21  13830  blres  13973  isxms2  13991  metrest  14045  metcnp  14051  txmetcnp  14057  txmetcn  14058  cnblcld  14074  reopnap  14077  ioocosf1o  14314  lgseisenlem2  14490  bj-nn0sucALT  14769  apdiff  14835