Theorem bitrdi 196

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitrdi.1	|- ( ph -> ( ps <-> ch ) )
bitrdi.2	|- ( ch <-> th )

Assertion

Ref	Expression
bitrdi	|- ( ph -> ( ps <-> th ) )

Proof of Theorem bitrdi

Step	Hyp	Ref	Expression
1		bitrdi.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		bitrdi.2	. . 3 |- ( ch <-> th )
3	2	a1i 9	. 2 |- ( ph -> ( ch <-> th ) )
4	1, 3	bitrd 188	1 |- ( ph -> ( ps <-> 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:  bitr2di  197  bitr4di  198  3bitr3g  222  bibi2i  227  ibibr  246  biancomd  271  imanst  889  pm5.75  964  xordidc  1418  19.17  1578  alexdc  1641  nf4dc  1692  abeq2d  2317  cbvralf  2729  cbvrexf  2730  cbvreu  2735  cbvrab  2769  ceqsralt  2798  ralab2  2936  rexab2  2938  euxfr2dc  2957  reu7  2967  reu8  2968  cbvralcsf  3155  cbvrexcsf  3156  cbvreucsf  3157  cbvrabcsf  3158  ralss  3258  rexss  3259  prssg  3789  2ralunsn  3838  eluniab  3861  elintab  3895  dfiun2g  3958  dfiin2g  3959  cbvopab1  4116  cbvmpt  4138  axsep2  4162  bnd2  4216  opeqsn  4295  reusv3  4505  tfisi  4633  opeliunxp  4728  eliunxp  4815  relop  4826  eldm2g  4872  reldm0  4894  relrn0  4938  restidsing  5012  xpmlem  5100  elxp5  5168  cnvpom  5222  cbviota  5234  iota1  5243  sniota  5259  fncnv  5334  fnres  5386  brprcneu  5563  fnopfvb  5614  fvelrnb  5620  fvelimab  5629  fvopab3g  5646  eqfnfv3  5673  eqfnfv2f  5675  fvreseq  5677  fnreseql  5684  rexsupp  5698  respreima  5702  rexrn  5711  ralrn  5712  f1ompt  5725  fsn  5746  fconstfvm  5792  fconst3m  5793  fconst4m  5794  foima2  5810  rexima  5813  ralima  5814  dff13  5827  foeqcnvco  5849  fliftfun  5855  isocnv  5870  isoini  5877  f1oiso  5885  cbvriota  5900  eusvobj2  5920  oprabid  5966  eloprabga  6022  resoprab  6031  eqfnov  6042  eqfnov2  6043  ov6g  6074  funimassov  6086  ovelimab  6087  caovord2  6109  uchoice  6213  releldm2  6261  dfoprab4  6268  xporderlem  6307  poxp  6308  f1od2  6311  mpoxopovel  6317  brtpos2  6327  brtpos0  6328  rntpos  6333  dftpos3  6338  tpostpos  6340  tpossym  6352  tposoprab  6356  tfrcllemres  6438  frecabcl  6475  frecsuclem  6482  erth2  6657  qliftfun  6694  erovlem  6704  ecopovsym  6708  ecopovsymg  6711  th3qlem1  6714  mapdm0  6740  elpmg  6741  elpm2g  6742  map0e  6763  dom2lem  6849  mapsnen  6888  xpdom2  6908  xpf1o  6923  mapen  6925  ssfilem  6954  diffitest  6966  ac6sfi  6977  ss1o0el1o  6992  isoti  7091  cnvti  7103  omp1eomlem  7178  ismkvnex  7239  nninfwlporlemd  7256  netap  7348  2omotaplemap  7351  ltexpi  7432  ordpipqqs  7469  ltexnqq  7503  enq0enq  7526  enq0sym  7527  enq0tr  7529  nqnq0pi  7533  genipv  7604  genprndl  7616  genprndu  7617  genpdisj  7618  genpassl  7619  genpassu  7620  addcomprg  7673  mulcomprg  7675  ltnqpr  7688  ltnqpri  7689  ltexprlemm  7695  ltexprlemdisj  7701  suplocexprlemmu  7813  suplocexprlemdisj  7815  ltsrprg  7842  mulgt0sr  7873  elreal2  7925  ltresr  7934  ltresr2  7935  axprecex  7975  axpre-ltadd  7981  axpre-mulgt0  7982  axpre-mulext  7983  axpre-suploclemres  7996  subcan2  8279  negcon1  8306  negcon2  8307  lt0neg1  8523  lt0neg2  8524  le0neg1  8525  le0neg2  8526  reapirr  8632  reapmul1  8650  reapneg  8652  remulext1  8654  apti  8677  negap0  8685  divmulap2  8731  reclt1  8951  recgt1  8952  suprleubex  9009  addltmul  9256  elznn0  9369  zapne  9429  zltlen  9433  nn0lt10b  9435  nn0lt2  9436  eluz1  9634  raluz  9681  rexuz  9683  qltlen  9743  cnref1o  9754  rpnegap  9790  ltxr  9879  xlt0neg1  9942  xlt0neg2  9943  xle0neg1  9944  xle0neg2  9945  elixx1  10001  elixx3g  10005  elioo2  10025  icc0r  10030  elicc4  10044  elioopnf  10071  elioomnf  10072  iooneg  10092  iccneg  10093  iccshftr  10098  iccshftl  10100  iccdil  10102  icccntr  10104  iccf1o  10108  elfz1  10117  0fz1  10149  fzpr  10181  fzdifsuc  10185  uzsplit  10196  elfzm1b  10202  elfzp12  10203  fznn0  10217  exfzdc  10350  zsupcllemstep  10353  flqeqceilz  10444  zmodid2  10478  expap0  10695  qsqeqor  10776  bernneq  10786  hasheqf1o  10911  hashfacen  10962  ccatrn  11040  sqrtmsq2i  11365  maxclpr  11452  minmax  11460  xrmaxlesup  11489  xrnegiso  11492  xrnegcon1d  11494  xrminmax  11495  clim0  11515  climrecvg1n  11578  summodc  11613  fsumsplit  11637  mertenslem2  11766  prodmodc  11808  fprodsplitdc  11826  fprod2dlemstep  11852  dvdsval2  12020  odd2np1lem  12102  even2n  12104  divalgb  12155  divalgmod  12157  bitsval  12173  bitsmod  12186  gcddvds  12203  bezoutlemmain  12238  nnwofdc  12278  isprm3  12359  prmind2  12361  dvdsprime  12363  coprm  12385  prmdvdsexp  12389  sqrt2irr  12403  sqpweven  12416  2sqpwodd  12417  pythagtriplem2  12508  pythagtrip  12525  pceu  12537  pc11  12573  elrest  12996  grpsubeq0  13336  grpsubadd  13338  issubg3  13446  isnsg  13456  eqger  13478  eqglact  13479  eqgid  13480  srgfcl  13653  dvdsrtr  13781  dvdsr02  13785  isunitd  13786  isrhm  13838  isrim0  13841  subsubrng2  13895  subsubrg2  13926  issubrg3  13927  opprdomnbg  13954  2idlelb  14185  mplelbascoe  14372  istopon  14403  isbasis2g  14435  isbasis3g  14436  tgss2  14469  bastop1  14473  iscld  14493  ntreq0  14522  restsn  14570  restopn2  14573  lmbr  14603  cnptoprest2  14630  txbas  14648  eltx  14649  txlm  14669  ishmeo  14694  hmeoimaf1o  14704  ispsmet  14713  ismet  14734  isxmet  14735  ismet2  14744  metn0  14768  elblps  14780  elbl  14781  bdbl  14893  qtopbasss  14911  elcncf  14963  ellimc3apf  15050  elply  15124  sincosq1sgn  15216  sincosq2sgn  15217  cos11  15243  logrpap0b  15266  lgsdir2lem4  15426  gausslemma2dlem0i  15452  lgsquadlem2  15473  m1lgs  15480  2lgsoddprmlem3  15506  2sqlem6  15515  2sqlem9  15519  2sqlem10  15520  2omap  15796  subctctexmid  15801  iooref1o  15837  iswomni0  15854