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  2798  ceqsralt  2828  ralab2  2968  rexab2  2970  euxfr2dc  2989  reu7  2999  reu8  3000  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  ralss  3291  rexss  3292  elif  3615  prssg  3828  2ralunsn  3880  eluniab  3903  elintab  3937  dfiun2g  4000  dfiin2g  4001  cbvopab1  4160  cbvmpt  4182  axsep2  4206  bnd2  4261  opeqsn  4343  reusv3  4555  tfisi  4683  opeliunxp  4779  eliunxp  4867  relop  4878  eldm2g  4925  reldm0  4947  relrn0  4992  restidsing  5067  xpmlem  5155  elxp5  5223  cnvpom  5277  cbviota  5289  iota1  5299  sniota  5315  fncnv  5393  fnres  5446  brprcneu  5628  fnopfvb  5681  fvelrnb  5689  fvelimab  5698  fvopab3g  5715  eqfnfv3  5742  eqfnfv2f  5744  fvreseq  5746  fnreseql  5753  rexsupp  5767  respreima  5771  rexrn  5780  ralrn  5781  f1ompt  5794  fsn  5815  fconstfvm  5867  fconst3m  5868  fconst4m  5869  foima2  5887  rexima  5890  ralima  5891  dff13  5904  foeqcnvco  5926  fliftfun  5932  isocnv  5947  isoini  5954  f1oiso  5962  cbvriota  5978  riotaeqimp  5991  eusvobj2  5999  oprabid  6045  eloprabga  6103  resoprab  6112  eqfnov  6123  eqfnov2  6124  ov6g  6155  funimassov  6167  ovelimab  6168  caovord2  6190  uchoice  6295  releldm2  6343  dfoprab4  6350  xporderlem  6391  poxp  6392  f1od2  6395  mpoxopovel  6402  brtpos2  6412  brtpos0  6413  rntpos  6418  dftpos3  6423  tpostpos  6425  tpossym  6437  tposoprab  6441  tfrcllemres  6523  frecabcl  6560  frecsuclem  6567  erth2  6744  qliftfun  6781  erovlem  6791  ecopovsym  6795  ecopovsymg  6798  th3qlem1  6801  mapdm0  6827  elpmg  6828  elpm2g  6829  map0e  6850  dom2lem  6940  mapsnen  6981  xpdom2  7010  xpf1o  7025  mapen  7027  ssfilem  7057  diffitest  7069  ac6sfi  7080  eqsndc  7088  ss1o0el1o  7098  isoti  7197  cnvti  7209  omp1eomlem  7284  ismkvnex  7345  nninfwlporlemd  7362  en2prde  7389  netap  7463  2omotaplemap  7466  ltexpi  7547  ordpipqqs  7584  ltexnqq  7618  enq0enq  7641  enq0sym  7642  enq0tr  7644  nqnq0pi  7648  genipv  7719  genprndl  7731  genprndu  7732  genpdisj  7733  genpassl  7734  genpassu  7735  addcomprg  7788  mulcomprg  7790  ltnqpr  7803  ltnqpri  7804  ltexprlemm  7810  ltexprlemdisj  7816  suplocexprlemmu  7928  suplocexprlemdisj  7930  ltsrprg  7957  mulgt0sr  7988  elreal2  8040  ltresr  8049  ltresr2  8050  axprecex  8090  axpre-ltadd  8096  axpre-mulgt0  8097  axpre-mulext  8098  axpre-suploclemres  8111  subcan2  8394  negcon1  8421  negcon2  8422  lt0neg1  8638  lt0neg2  8639  le0neg1  8640  le0neg2  8641  reapirr  8747  reapmul1  8765  reapneg  8767  remulext1  8769  apti  8792  negap0  8800  divmulap2  8846  reclt1  9066  recgt1  9067  suprleubex  9124  addltmul  9371  elznn0  9484  zapne  9544  zltlen  9548  nn0lt10b  9550  nn0lt2  9551  eluz1  9749  raluz  9802  rexuz  9804  qltlen  9864  cnref1o  9875  rpnegap  9911  ltxr  10000  xlt0neg1  10063  xlt0neg2  10064  xle0neg1  10065  xle0neg2  10066  elixx1  10122  elixx3g  10126  elioo2  10146  icc0r  10151  elicc4  10165  elioopnf  10192  elioomnf  10193  iooneg  10213  iccneg  10214  iccshftr  10219  iccshftl  10221  iccdil  10223  icccntr  10225  iccf1o  10229  elfz1  10238  0fz1  10270  fzpr  10302  fzdifsuc  10306  uzsplit  10317  elfzm1b  10323  elfzp12  10324  fznn0  10338  exfzdc  10476  zsupcllemstep  10479  flqeqceilz  10570  zmodid2  10604  expap0  10821  qsqeqor  10902  bernneq  10912  hasheqf1o  11037  hashfacen  11090  ccatrn  11176  pfxsuffeqwrdeq  11269  wrd2ind  11294  sqrtmsq2i  11686  maxclpr  11773  minmax  11781  xrmaxlesup  11810  xrnegiso  11813  xrnegcon1d  11815  xrminmax  11816  clim0  11836  climrecvg1n  11899  summodc  11934  fsumsplit  11958  mertenslem2  12087  prodmodc  12129  fprodsplitdc  12147  fprod2dlemstep  12173  dvdsval2  12341  odd2np1lem  12423  even2n  12425  divalgb  12476  divalgmod  12478  bitsval  12494  bitsmod  12507  gcddvds  12524  bezoutlemmain  12559  nnwofdc  12599  isprm3  12680  prmind2  12682  dvdsprime  12684  coprm  12706  prmdvdsexp  12710  sqrt2irr  12724  sqpweven  12737  2sqpwodd  12738  pythagtriplem2  12829  pythagtrip  12846  pceu  12858  pc11  12894  elrest  13319  grpsubeq0  13659  grpsubadd  13661  issubg3  13769  isnsg  13779  eqger  13801  eqglact  13802  eqgid  13803  srgfcl  13976  dvdsrtr  14105  dvdsr02  14109  isunitd  14110  isrhm  14162  isrim0  14165  subsubrng2  14219  subsubrg2  14250  issubrg3  14251  opprdomnbg  14278  2idlelb  14509  mplelbascoe  14696  istopon  14727  isbasis2g  14759  isbasis3g  14760  tgss2  14793  bastop1  14797  iscld  14817  ntreq0  14846  restsn  14894  restopn2  14897  lmbr  14927  cnptoprest2  14954  txbas  14972  eltx  14973  txlm  14993  ishmeo  15018  hmeoimaf1o  15028  ispsmet  15037  ismet  15058  isxmet  15059  ismet2  15068  metn0  15092  elblps  15104  elbl  15105  bdbl  15217  qtopbasss  15235  elcncf  15287  ellimc3apf  15374  elply  15448  sincosq1sgn  15540  sincosq2sgn  15541  cos11  15567  logrpap0b  15590  lgsdir2lem4  15750  gausslemma2dlem0i  15776  lgsquadlem2  15797  m1lgs  15804  2lgsoddprmlem3  15830  2sqlem6  15839  2sqlem9  15843  2sqlem10  15844  vtxdfifiun  16103  wlkl1loop  16155  wlkv0  16166  wlklenvclwlk  16170  upgr2wlkdc  16172  isclwwlk  16189  isclwwlkng  16201  isclwwlknx  16211  clwwlkn2  16216  2omap  16530  pw1map  16532  subctctexmid  16537  iooref1o  16574  iswomni0  16591