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  3826  2ralunsn  3878  eluniab  3901  elintab  3935  dfiun2g  3998  dfiin2g  3999  cbvopab1  4158  cbvmpt  4180  axsep2  4204  bnd2  4259  opeqsn  4341  reusv3  4553  tfisi  4681  opeliunxp  4777  eliunxp  4865  relop  4876  eldm2g  4923  reldm0  4945  relrn0  4990  restidsing  5065  xpmlem  5153  elxp5  5221  cnvpom  5275  cbviota  5287  iota1  5297  sniota  5313  fncnv  5391  fnres  5444  brprcneu  5626  fnopfvb  5679  fvelrnb  5687  fvelimab  5696  fvopab3g  5713  eqfnfv3  5740  eqfnfv2f  5742  fvreseq  5744  fnreseql  5751  rexsupp  5765  respreima  5769  rexrn  5778  ralrn  5779  f1ompt  5792  fsn  5813  fconstfvm  5865  fconst3m  5866  fconst4m  5867  foima2  5885  rexima  5888  ralima  5889  dff13  5902  foeqcnvco  5924  fliftfun  5930  isocnv  5945  isoini  5952  f1oiso  5960  cbvriota  5976  riotaeqimp  5989  eusvobj2  5997  oprabid  6043  eloprabga  6101  resoprab  6110  eqfnov  6121  eqfnov2  6122  ov6g  6153  funimassov  6165  ovelimab  6166  caovord2  6188  uchoice  6293  releldm2  6341  dfoprab4  6348  xporderlem  6389  poxp  6390  f1od2  6393  mpoxopovel  6400  brtpos2  6410  brtpos0  6411  rntpos  6416  dftpos3  6421  tpostpos  6423  tpossym  6435  tposoprab  6439  tfrcllemres  6521  frecabcl  6558  frecsuclem  6565  erth2  6742  qliftfun  6779  erovlem  6789  ecopovsym  6793  ecopovsymg  6796  th3qlem1  6799  mapdm0  6825  elpmg  6826  elpm2g  6827  map0e  6848  dom2lem  6938  mapsnen  6979  xpdom2  7008  xpf1o  7023  mapen  7025  ssfilem  7055  diffitest  7067  ac6sfi  7078  eqsndc  7086  ss1o0el1o  7096  isoti  7195  cnvti  7207  omp1eomlem  7282  ismkvnex  7343  nninfwlporlemd  7360  en2prde  7387  netap  7461  2omotaplemap  7464  ltexpi  7545  ordpipqqs  7582  ltexnqq  7616  enq0enq  7639  enq0sym  7640  enq0tr  7642  nqnq0pi  7646  genipv  7717  genprndl  7729  genprndu  7730  genpdisj  7731  genpassl  7732  genpassu  7733  addcomprg  7786  mulcomprg  7788  ltnqpr  7801  ltnqpri  7802  ltexprlemm  7808  ltexprlemdisj  7814  suplocexprlemmu  7926  suplocexprlemdisj  7928  ltsrprg  7955  mulgt0sr  7986  elreal2  8038  ltresr  8047  ltresr2  8048  axprecex  8088  axpre-ltadd  8094  axpre-mulgt0  8095  axpre-mulext  8096  axpre-suploclemres  8109  subcan2  8392  negcon1  8419  negcon2  8420  lt0neg1  8636  lt0neg2  8637  le0neg1  8638  le0neg2  8639  reapirr  8745  reapmul1  8763  reapneg  8765  remulext1  8767  apti  8790  negap0  8798  divmulap2  8844  reclt1  9064  recgt1  9065  suprleubex  9122  addltmul  9369  elznn0  9482  zapne  9542  zltlen  9546  nn0lt10b  9548  nn0lt2  9549  eluz1  9747  raluz  9800  rexuz  9802  qltlen  9862  cnref1o  9873  rpnegap  9909  ltxr  9998  xlt0neg1  10061  xlt0neg2  10062  xle0neg1  10063  xle0neg2  10064  elixx1  10120  elixx3g  10124  elioo2  10144  icc0r  10149  elicc4  10163  elioopnf  10190  elioomnf  10191  iooneg  10211  iccneg  10212  iccshftr  10217  iccshftl  10219  iccdil  10221  icccntr  10223  iccf1o  10227  elfz1  10236  0fz1  10268  fzpr  10300  fzdifsuc  10304  uzsplit  10315  elfzm1b  10321  elfzp12  10322  fznn0  10336  exfzdc  10474  zsupcllemstep  10477  flqeqceilz  10568  zmodid2  10602  expap0  10819  qsqeqor  10900  bernneq  10910  hasheqf1o  11035  hashfacen  11087  ccatrn  11173  pfxsuffeqwrdeq  11266  wrd2ind  11291  sqrtmsq2i  11683  maxclpr  11770  minmax  11778  xrmaxlesup  11807  xrnegiso  11810  xrnegcon1d  11812  xrminmax  11813  clim0  11833  climrecvg1n  11896  summodc  11931  fsumsplit  11955  mertenslem2  12084  prodmodc  12126  fprodsplitdc  12144  fprod2dlemstep  12170  dvdsval2  12338  odd2np1lem  12420  even2n  12422  divalgb  12473  divalgmod  12475  bitsval  12491  bitsmod  12504  gcddvds  12521  bezoutlemmain  12556  nnwofdc  12596  isprm3  12677  prmind2  12679  dvdsprime  12681  coprm  12703  prmdvdsexp  12707  sqrt2irr  12721  sqpweven  12734  2sqpwodd  12735  pythagtriplem2  12826  pythagtrip  12843  pceu  12855  pc11  12891  elrest  13316  grpsubeq0  13656  grpsubadd  13658  issubg3  13766  isnsg  13776  eqger  13798  eqglact  13799  eqgid  13800  srgfcl  13973  dvdsrtr  14102  dvdsr02  14106  isunitd  14107  isrhm  14159  isrim0  14162  subsubrng2  14216  subsubrg2  14247  issubrg3  14248  opprdomnbg  14275  2idlelb  14506  mplelbascoe  14693  istopon  14724  isbasis2g  14756  isbasis3g  14757  tgss2  14790  bastop1  14794  iscld  14814  ntreq0  14843  restsn  14891  restopn2  14894  lmbr  14924  cnptoprest2  14951  txbas  14969  eltx  14970  txlm  14990  ishmeo  15015  hmeoimaf1o  15025  ispsmet  15034  ismet  15055  isxmet  15056  ismet2  15065  metn0  15089  elblps  15101  elbl  15102  bdbl  15214  qtopbasss  15232  elcncf  15284  ellimc3apf  15371  elply  15445  sincosq1sgn  15537  sincosq2sgn  15538  cos11  15564  logrpap0b  15587  lgsdir2lem4  15747  gausslemma2dlem0i  15773  lgsquadlem2  15794  m1lgs  15801  2lgsoddprmlem3  15827  2sqlem6  15836  2sqlem9  15840  2sqlem10  15841  vtxdfifiun  16099  wlkl1loop  16146  wlkv0  16157  wlklenvclwlk  16161  upgr2wlkdc  16163  isclwwlk  16179  isclwwlkng  16191  isclwwlknx  16201  clwwlkn2  16206  2omap  16504  pw1map  16506  subctctexmid  16511  iooref1o  16548  iswomni0  16565