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  906  dn1dc  963  bilukdc  1416  nf4dc  1694  sbal1  2031  abbi  2320  necon3abid  2416  necon3bid  2418  necon1abiidc  2437  r19.21t  2582  ceqsralt  2801  ceqsrexv  2907  ceqsrex2v  2909  elab2g  2924  elrabf  2931  eueq2dc  2950  euxfrdc  2963  eqreu  2969  reu8  2973  ru  3001  sbcralt  3079  sbcrext  3080  sbcne12g  3115  csbnestgf  3150  dfss4st  3410  rexsng  3679  ralprg  3689  rexprg  3690  difsn  3776  opthpr  3819  ralunsn  3844  dfiin2g  3966  iunxsng  4009  iunxsngf  4011  elpwuni  4023  pwnss  4211  exmid01  4250  opelopabt  4316  opelopabga  4317  brabga  4318  opelopabgf  4324  elsucg  4459  elsuc2g  4460  brab2a  4736  opeliunxp  4738  posng  4755  brab2ga  4758  csbdmg  4881  elrnmpt1  4938  elrnmptg  4939  eliniseg2  5071  poleloe  5091  elxp4  5179  elxp5  5180  cnvpom  5234  sbcfung  5304  dffun8  5308  fncnv  5349  fununi  5351  fnssresb  5397  fnimaeq0  5407  funcocnv2  5559  dffn5im  5637  funimass4  5642  fnsnfv  5651  dmfco  5660  fndmdif  5698  fndmin  5700  unpreima  5718  respreima  5721  fsn2  5767  fnressn  5783  fressnfv  5784  elunirn  5848  dff13  5850  fliftel  5875  isoini  5900  f1oiso  5908  acexmid  5956  eloprabga  6045  resoprab2  6055  ralrnmpo  6073  rexrnmpo  6074  ovid  6075  ov  6078  ovg  6098  ofrfval2  6188  fmpox  6299  1stconst  6320  2ndconst  6321  f1od2  6334  rbropapd  6341  brtpos2  6350  dfsmo2  6386  frecabcl  6498  brdifun  6660  eqerlem  6664  brecop  6725  erovlem  6727  mapsn  6790  mptelixpg  6834  map1  6918  xpsnen  6931  xpdom2  6941  xpf1o  6956  supubti  7116  infglbti  7142  ctssdccl  7228  nninfwlpoim  7296  nninfinfwlpo  7297  netap  7386  2omotaplemap  7389  ltpiord  7452  nlt1pig  7474  elinp  7607  ltdfpr  7639  genpassl  7657  genpassu  7658  1idprl  7723  1idpru  7724  gt0srpr  7881  mappsrprg  7937  map2psrprg  7938  peano2nnnn  7986  recidpirq  7991  axprecex  8013  xrlenlt  8157  addsubeq4  8307  renegcl  8353  lesub0  8572  recexaplem2  8745  conjmulap  8822  rerecclap  8823  creui  9053  peano2nn  9068  nndiv  9097  elznn0  9407  eqreznegel  9755  negelrp  9829  ltxr  9917  divelunit  10144  iccf1o  10146  elfz2  10157  elfzp1  10214  fzdifsuc  10223  fznn  10231  nelfzo  10294  fzosplitsni  10386  fvinim0ffz  10392  infssuzex  10398  zsupssdc  10403  frec2uzisod  10574  sq11i  10796  wrdval  11019  csbwrdg  11045  swrdnd  11135  wrd2ind  11199  cjreb  11252  rexfiuz  11375  cau3lem  11500  pwm1geoserap1  11894  mertensabs  11923  divides  12175  dvdsabseq  12233  odd2np1  12259  oddm1even  12261  modremain  12315  bezoutlemnewy  12392  bezoutlemstep  12393  bezoutlemmain  12394  bezoutlema  12395  bezoutlemb  12396  isprm2  12514  isprm4  12516  dvdsnprmd  12522  oddprmdvds  12752  4sqlem2  12787  4sqlem12  12800  xpsfrnel2  13253  issubm  13379  grplmulf1o  13481  grplactcnv  13509  issubg  13584  elnmz  13619  isghm  13654  ghmeqker  13682  srg1zr  13824  iscrng2  13852  issubrng  14036  aprval  14119  zndvds  14486  znleval  14490  psrbag  14506  istopg  14546  basgen2  14628  isnei  14691  restdis  14731  iscn  14744  iscnp  14746  lmbr2  14761  lmbrf  14762  txcn  14822  cnmpt21  14838  blres  14981  isxms2  14999  metrest  15053  metcnp  15059  txmetcnp  15065  txmetcn  15066  cnblcld  15082  reopnap  15093  ioocosf1o  15401  mpodvdsmulf1o  15537  gausslemma2dlem0i  15609  gausslemma2dlem1a  15610  lgseisenlem2  15623  lgsquadlem1  15629  lgsquadlem2  15630  2lgslem1a  15640  isuhgrm  15742  isushgrm  15743  isupgren  15766  isumgren  15776  bj-nn0sucALT  16052  apdiff  16128