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  916  dn1dc  973  bilukdc  1445  nf4dc  1722  sbal1  2062  abbibcom  2352  abbib  2356  necon3abid  2459  necon3bid  2461  necon1abiidc  2480  r19.21t  2625  ceqsralt  2849  ceqsrexv  2956  ceqsrex2v  2958  elab2g  2973  elrabf  2980  eueq2dc  2999  euxfrdc  3012  eqreu  3018  reu8  3022  ru  3050  sbcralt  3128  sbcrext  3129  sbcne12g  3165  csbnestgf  3200  dfss4st  3464  rexsng  3746  ralprg  3756  rexprg  3757  difsn  3847  opthpr  3892  ralunsn  3918  dfiin2g  4040  iunxsng  4083  iunxsngf  4085  elpwuni  4097  pwnss  4291  exmid01  4330  opelopabt  4399  opelopabga  4400  brabga  4401  opelopabgf  4407  elsucg  4544  elsuc2g  4545  brab2a  4823  opeliunxp  4825  posng  4842  brab2ga  4845  csbdmg  4970  elrnmpt1  5028  elrnmptg  5029  eliniseg2  5162  poleloe  5182  elxp4  5270  elxp5  5271  cnvpom  5325  sbcfung  5396  dffun8  5400  fncnv  5442  fununi  5444  fnssresb  5490  fnimaeq0  5500  funcocnv2  5659  dffn5im  5742  funimass4  5747  fnsnfv  5756  dmfco  5767  fndmdif  5805  fndmin  5807  unpreima  5824  respreima  5827  fsn2  5873  fnressn  5892  fressnfv  5893  elunirn  5962  dff13  5964  fliftel  5989  isoini  6014  f1oiso  6022  riotaeqimp  6053  acexmid  6074  fnbrovb  6120  eloprabga  6165  resoprab2  6175  ralrnmpo  6193  rexrnmpo  6194  ovid  6195  ov  6198  ovg  6218  ofrfval2  6309  fmpox  6426  1stconst  6447  2ndconst  6448  f1od2  6461  rbropapd  6503  brtpos2  6512  dfsmo2  6548  frecabcl  6660  brdifun  6824  eqerlem  6828  brecop  6889  erovlem  6891  mapfset  6935  mapsnd  6960  mapsn  6962  mptelixpg  7006  map1  7091  xpsnen  7109  xpdom2  7119  xpf1o  7134  mapunen  7141  supubti  7329  infglbti  7355  ctssdccl  7441  nninfwlpoim  7509  nninfinfwlpo  7510  netap  7610  2omotaplemap  7613  ltpiord  7676  nlt1pig  7698  elinp  7831  ltdfpr  7863  genpassl  7881  genpassu  7882  1idprl  7947  1idpru  7948  gt0srpr  8105  mappsrprg  8161  map2psrprg  8162  peano2nnnn  8210  recidpirq  8215  axprecex  8237  xrlenlt  8380  addsubeq4  8531  renegcl  8577  lesub0  8797  recexaplem2  8970  conjmulap  9049  rerecclap  9050  creui  9280  peano2nn  9295  nndiv  9324  elznn0  9638  eqreznegel  9993  negelrp  10067  ltxr  10156  divelunit  10383  iccf1o  10386  elfz2  10397  elfzp1  10457  fzdifsuc  10466  fznn  10474  nelfzo  10537  fzosplitsni  10632  fvinim0ffz  10638  infssuzex  10644  zsupssdc  10651  frec2uzisod  10822  sq11i  11044  wrdval  11285  csbwrdg  11312  swrdnd  11409  wrd2ind  11473  cjreb  11609  rexfiuz  11733  cau3lem  11858  pwm1geoserap1  12253  mertensabs  12282  divides  12534  dvdsabseq  12592  odd2np1  12618  oddm1even  12620  modremain  12674  bezoutlemnewy  12751  bezoutlemstep  12752  bezoutlemmain  12753  bezoutlema  12754  bezoutlemb  12755  isprm2  12873  isprm4  12875  dvdsnprmd  12881  oddprmdvds  13111  4sqlem2  13146  4sqlem12  13159  xpsfrnel2  13644  issubm  13756  grplmulf1o  13856  grplactcnv  13884  issubg  13953  elnmz  13988  isghm  14023  ghmeqker  14051  rng1zrlem  14233  iscrng2  14293  issubrng  14480  aprval  14564  zndvds  14956  znleval  14960  psrbag  14976  istopg  15023  basgen2  15105  isnei  15168  restdis  15208  iscn  15221  iscnp  15223  lmbr2  15238  lmbrf  15239  txcn  15299  cnmpt21  15315  blres  15458  isxms2  15476  metrest  15530  metcnp  15536  txmetcnp  15542  txmetcn  15543  cnblcld  15559  reopnap  15570  ioocosf1o  15878  mpodvdsmulf1o  16018  gausslemma2dlem0i  16090  gausslemma2dlem1a  16091  lgseisenlem2  16104  lgsquadlem1  16110  lgsquadlem2  16111  2lgslem1a  16121  isuhgrm  16226  isushgrm  16227  isupgren  16250  isumgren  16260  isuspgren  16312  isusgren  16313  uhgr0v0e  16389  vtxdg0v  16449  iswlk  16478  wlk1walkdom  16514  istrl  16540  clwwlkn1  16573  clwwlkn2  16576  clwwlknonel  16587  clwwlknun  16596  iseupth  16602  eupthres  16612  eupth2lem1  16613  eupth2lemsfi  16633  bj-nn0sucALT  16918  apdiff  17002