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  893  pm5.75  968  xordidc  1441  19.17  1602  alexdc  1665  nf4dc  1716  abeq2d  2342  cbvralf  2756  cbvrexf  2757  cbvreu  2763  cbvrab  2797  ceqsralt  2827  ralab2  2967  rexab2  2969  euxfr2dc  2988  reu7  2998  reu8  2999  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  ralss  3290  rexss  3291  elif  3614  prssg  3825  2ralunsn  3877  eluniab  3900  elintab  3934  dfiun2g  3997  dfiin2g  3998  cbvopab1  4157  cbvmpt  4179  axsep2  4203  bnd2  4257  opeqsn  4339  reusv3  4551  tfisi  4679  opeliunxp  4774  eliunxp  4861  relop  4872  eldm2g  4919  reldm0  4941  relrn0  4986  restidsing  5061  xpmlem  5149  elxp5  5217  cnvpom  5271  cbviota  5283  iota1  5293  sniota  5309  fncnv  5387  fnres  5440  brprcneu  5622  fnopfvb  5675  fvelrnb  5683  fvelimab  5692  fvopab3g  5709  eqfnfv3  5736  eqfnfv2f  5738  fvreseq  5740  fnreseql  5747  rexsupp  5761  respreima  5765  rexrn  5774  ralrn  5775  f1ompt  5788  fsn  5809  fconstfvm  5861  fconst3m  5862  fconst4m  5863  foima2  5881  rexima  5884  ralima  5885  dff13  5898  foeqcnvco  5920  fliftfun  5926  isocnv  5941  isoini  5948  f1oiso  5956  cbvriota  5972  riotaeqimp  5985  eusvobj2  5993  oprabid  6039  eloprabga  6097  resoprab  6106  eqfnov  6117  eqfnov2  6118  ov6g  6149  funimassov  6161  ovelimab  6162  caovord2  6184  uchoice  6289  releldm2  6337  dfoprab4  6344  xporderlem  6383  poxp  6384  f1od2  6387  mpoxopovel  6393  brtpos2  6403  brtpos0  6404  rntpos  6409  dftpos3  6414  tpostpos  6416  tpossym  6428  tposoprab  6432  tfrcllemres  6514  frecabcl  6551  frecsuclem  6558  erth2  6735  qliftfun  6772  erovlem  6782  ecopovsym  6786  ecopovsymg  6789  th3qlem1  6792  mapdm0  6818  elpmg  6819  elpm2g  6820  map0e  6841  dom2lem  6931  mapsnen  6972  xpdom2  6998  xpf1o  7013  mapen  7015  ssfilem  7045  diffitest  7057  ac6sfi  7068  eqsndc  7076  ss1o0el1o  7086  isoti  7185  cnvti  7197  omp1eomlem  7272  ismkvnex  7333  nninfwlporlemd  7350  en2prde  7377  netap  7451  2omotaplemap  7454  ltexpi  7535  ordpipqqs  7572  ltexnqq  7606  enq0enq  7629  enq0sym  7630  enq0tr  7632  nqnq0pi  7636  genipv  7707  genprndl  7719  genprndu  7720  genpdisj  7721  genpassl  7722  genpassu  7723  addcomprg  7776  mulcomprg  7778  ltnqpr  7791  ltnqpri  7792  ltexprlemm  7798  ltexprlemdisj  7804  suplocexprlemmu  7916  suplocexprlemdisj  7918  ltsrprg  7945  mulgt0sr  7976  elreal2  8028  ltresr  8037  ltresr2  8038  axprecex  8078  axpre-ltadd  8084  axpre-mulgt0  8085  axpre-mulext  8086  axpre-suploclemres  8099  subcan2  8382  negcon1  8409  negcon2  8410  lt0neg1  8626  lt0neg2  8627  le0neg1  8628  le0neg2  8629  reapirr  8735  reapmul1  8753  reapneg  8755  remulext1  8757  apti  8780  negap0  8788  divmulap2  8834  reclt1  9054  recgt1  9055  suprleubex  9112  addltmul  9359  elznn0  9472  zapne  9532  zltlen  9536  nn0lt10b  9538  nn0lt2  9539  eluz1  9737  raluz  9785  rexuz  9787  qltlen  9847  cnref1o  9858  rpnegap  9894  ltxr  9983  xlt0neg1  10046  xlt0neg2  10047  xle0neg1  10048  xle0neg2  10049  elixx1  10105  elixx3g  10109  elioo2  10129  icc0r  10134  elicc4  10148  elioopnf  10175  elioomnf  10176  iooneg  10196  iccneg  10197  iccshftr  10202  iccshftl  10204  iccdil  10206  icccntr  10208  iccf1o  10212  elfz1  10221  0fz1  10253  fzpr  10285  fzdifsuc  10289  uzsplit  10300  elfzm1b  10306  elfzp12  10307  fznn0  10321  exfzdc  10458  zsupcllemstep  10461  flqeqceilz  10552  zmodid2  10586  expap0  10803  qsqeqor  10884  bernneq  10894  hasheqf1o  11019  hashfacen  11071  ccatrn  11157  pfxsuffeqwrdeq  11245  wrd2ind  11270  sqrtmsq2i  11661  maxclpr  11748  minmax  11756  xrmaxlesup  11785  xrnegiso  11788  xrnegcon1d  11790  xrminmax  11791  clim0  11811  climrecvg1n  11874  summodc  11909  fsumsplit  11933  mertenslem2  12062  prodmodc  12104  fprodsplitdc  12122  fprod2dlemstep  12148  dvdsval2  12316  odd2np1lem  12398  even2n  12400  divalgb  12451  divalgmod  12453  bitsval  12469  bitsmod  12482  gcddvds  12499  bezoutlemmain  12534  nnwofdc  12574  isprm3  12655  prmind2  12657  dvdsprime  12659  coprm  12681  prmdvdsexp  12685  sqrt2irr  12699  sqpweven  12712  2sqpwodd  12713  pythagtriplem2  12804  pythagtrip  12821  pceu  12833  pc11  12869  elrest  13294  grpsubeq0  13634  grpsubadd  13636  issubg3  13744  isnsg  13754  eqger  13776  eqglact  13777  eqgid  13778  srgfcl  13951  dvdsrtr  14080  dvdsr02  14084  isunitd  14085  isrhm  14137  isrim0  14140  subsubrng2  14194  subsubrg2  14225  issubrg3  14226  opprdomnbg  14253  2idlelb  14484  mplelbascoe  14671  istopon  14702  isbasis2g  14734  isbasis3g  14735  tgss2  14768  bastop1  14772  iscld  14792  ntreq0  14821  restsn  14869  restopn2  14872  lmbr  14902  cnptoprest2  14929  txbas  14947  eltx  14948  txlm  14968  ishmeo  14993  hmeoimaf1o  15003  ispsmet  15012  ismet  15033  isxmet  15034  ismet2  15043  metn0  15067  elblps  15079  elbl  15080  bdbl  15192  qtopbasss  15210  elcncf  15262  ellimc3apf  15349  elply  15423  sincosq1sgn  15515  sincosq2sgn  15516  cos11  15542  logrpap0b  15565  lgsdir2lem4  15725  gausslemma2dlem0i  15751  lgsquadlem2  15772  m1lgs  15779  2lgsoddprmlem3  15805  2sqlem6  15814  2sqlem9  15818  2sqlem10  15819  vtxdfifiun  16056  wlkl1loop  16099  wlkv0  16110  wlklenvclwlk  16114  upgr2wlkdc  16116  isclwwlk  16132  2omap  16418  pw1map  16420  subctctexmid  16425  iooref1o  16462  iswomni0  16479