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  4296  reusv3  4506  tfisi  4634  opeliunxp  4729  eliunxp  4816  relop  4827  eldm2g  4873  reldm0  4895  relrn0  4939  restidsing  5014  xpmlem  5102  elxp5  5170  cnvpom  5224  cbviota  5236  iota1  5245  sniota  5261  fncnv  5339  fnres  5391  brprcneu  5568  fnopfvb  5619  fvelrnb  5625  fvelimab  5634  fvopab3g  5651  eqfnfv3  5678  eqfnfv2f  5680  fvreseq  5682  fnreseql  5689  rexsupp  5703  respreima  5707  rexrn  5716  ralrn  5717  f1ompt  5730  fsn  5751  fconstfvm  5801  fconst3m  5802  fconst4m  5803  foima2  5819  rexima  5822  ralima  5823  dff13  5836  foeqcnvco  5858  fliftfun  5864  isocnv  5879  isoini  5886  f1oiso  5894  cbvriota  5909  eusvobj2  5929  oprabid  5975  eloprabga  6031  resoprab  6040  eqfnov  6051  eqfnov2  6052  ov6g  6083  funimassov  6095  ovelimab  6096  caovord2  6118  uchoice  6222  releldm2  6270  dfoprab4  6277  xporderlem  6316  poxp  6317  f1od2  6320  mpoxopovel  6326  brtpos2  6336  brtpos0  6337  rntpos  6342  dftpos3  6347  tpostpos  6349  tpossym  6361  tposoprab  6365  tfrcllemres  6447  frecabcl  6484  frecsuclem  6491  erth2  6666  qliftfun  6703  erovlem  6713  ecopovsym  6717  ecopovsymg  6720  th3qlem1  6723  mapdm0  6749  elpmg  6750  elpm2g  6751  map0e  6772  dom2lem  6862  mapsnen  6902  xpdom2  6925  xpf1o  6940  mapen  6942  ssfilem  6971  diffitest  6983  ac6sfi  6994  ss1o0el1o  7009  isoti  7108  cnvti  7120  omp1eomlem  7195  ismkvnex  7256  nninfwlporlemd  7273  netap  7365  2omotaplemap  7368  ltexpi  7449  ordpipqqs  7486  ltexnqq  7520  enq0enq  7543  enq0sym  7544  enq0tr  7546  nqnq0pi  7550  genipv  7621  genprndl  7633  genprndu  7634  genpdisj  7635  genpassl  7636  genpassu  7637  addcomprg  7690  mulcomprg  7692  ltnqpr  7705  ltnqpri  7706  ltexprlemm  7712  ltexprlemdisj  7718  suplocexprlemmu  7830  suplocexprlemdisj  7832  ltsrprg  7859  mulgt0sr  7890  elreal2  7942  ltresr  7951  ltresr2  7952  axprecex  7992  axpre-ltadd  7998  axpre-mulgt0  7999  axpre-mulext  8000  axpre-suploclemres  8013  subcan2  8296  negcon1  8323  negcon2  8324  lt0neg1  8540  lt0neg2  8541  le0neg1  8542  le0neg2  8543  reapirr  8649  reapmul1  8667  reapneg  8669  remulext1  8671  apti  8694  negap0  8702  divmulap2  8748  reclt1  8968  recgt1  8969  suprleubex  9026  addltmul  9273  elznn0  9386  zapne  9446  zltlen  9450  nn0lt10b  9452  nn0lt2  9453  eluz1  9651  raluz  9698  rexuz  9700  qltlen  9760  cnref1o  9771  rpnegap  9807  ltxr  9896  xlt0neg1  9959  xlt0neg2  9960  xle0neg1  9961  xle0neg2  9962  elixx1  10018  elixx3g  10022  elioo2  10042  icc0r  10047  elicc4  10061  elioopnf  10088  elioomnf  10089  iooneg  10109  iccneg  10110  iccshftr  10115  iccshftl  10117  iccdil  10119  icccntr  10121  iccf1o  10125  elfz1  10134  0fz1  10166  fzpr  10198  fzdifsuc  10202  uzsplit  10213  elfzm1b  10219  elfzp12  10220  fznn0  10234  exfzdc  10367  zsupcllemstep  10370  flqeqceilz  10461  zmodid2  10495  expap0  10712  qsqeqor  10793  bernneq  10803  hasheqf1o  10928  hashfacen  10979  ccatrn  11063  sqrtmsq2i  11388  maxclpr  11475  minmax  11483  xrmaxlesup  11512  xrnegiso  11515  xrnegcon1d  11517  xrminmax  11518  clim0  11538  climrecvg1n  11601  summodc  11636  fsumsplit  11660  mertenslem2  11789  prodmodc  11831  fprodsplitdc  11849  fprod2dlemstep  11875  dvdsval2  12043  odd2np1lem  12125  even2n  12127  divalgb  12178  divalgmod  12180  bitsval  12196  bitsmod  12209  gcddvds  12226  bezoutlemmain  12261  nnwofdc  12301  isprm3  12382  prmind2  12384  dvdsprime  12386  coprm  12408  prmdvdsexp  12412  sqrt2irr  12426  sqpweven  12439  2sqpwodd  12440  pythagtriplem2  12531  pythagtrip  12548  pceu  12560  pc11  12596  elrest  13020  grpsubeq0  13360  grpsubadd  13362  issubg3  13470  isnsg  13480  eqger  13502  eqglact  13503  eqgid  13504  srgfcl  13677  dvdsrtr  13805  dvdsr02  13809  isunitd  13810  isrhm  13862  isrim0  13865  subsubrng2  13919  subsubrg2  13950  issubrg3  13951  opprdomnbg  13978  2idlelb  14209  mplelbascoe  14396  istopon  14427  isbasis2g  14459  isbasis3g  14460  tgss2  14493  bastop1  14497  iscld  14517  ntreq0  14546  restsn  14594  restopn2  14597  lmbr  14627  cnptoprest2  14654  txbas  14672  eltx  14673  txlm  14693  ishmeo  14718  hmeoimaf1o  14728  ispsmet  14737  ismet  14758  isxmet  14759  ismet2  14768  metn0  14792  elblps  14804  elbl  14805  bdbl  14917  qtopbasss  14935  elcncf  14987  ellimc3apf  15074  elply  15148  sincosq1sgn  15240  sincosq2sgn  15241  cos11  15267  logrpap0b  15290  lgsdir2lem4  15450  gausslemma2dlem0i  15476  lgsquadlem2  15497  m1lgs  15504  2lgsoddprmlem3  15530  2sqlem6  15539  2sqlem9  15543  2sqlem10  15544  2omap  15865  subctctexmid  15870  iooref1o  15906  iswomni0  15923