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  1410  19.17  1570  alexdc  1633  nf4dc  1684  abeq2d  2309  cbvralf  2721  cbvrexf  2722  cbvreu  2727  cbvrab  2761  ceqsralt  2790  ralab2  2928  rexab2  2930  euxfr2dc  2949  reu7  2959  reu8  2960  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  ralss  3250  rexss  3251  prssg  3780  2ralunsn  3829  eluniab  3852  elintab  3886  dfiun2g  3949  dfiin2g  3950  cbvopab1  4107  cbvmpt  4129  axsep2  4153  bnd2  4207  opeqsn  4286  reusv3  4496  tfisi  4624  opeliunxp  4719  eliunxp  4806  relop  4817  eldm2g  4863  reldm0  4885  relrn0  4929  restidsing  5003  xpmlem  5091  elxp5  5159  cnvpom  5213  cbviota  5225  iota1  5234  sniota  5250  fncnv  5325  fnres  5377  brprcneu  5554  fnopfvb  5605  fvelrnb  5611  fvelimab  5620  fvopab3g  5637  eqfnfv3  5664  eqfnfv2f  5666  fvreseq  5668  fnreseql  5675  rexsupp  5689  respreima  5693  rexrn  5702  ralrn  5703  f1ompt  5716  fsn  5737  fconstfvm  5783  fconst3m  5784  fconst4m  5785  foima2  5801  rexima  5804  ralima  5805  dff13  5818  foeqcnvco  5840  fliftfun  5846  isocnv  5861  isoini  5868  f1oiso  5876  cbvriota  5891  eusvobj2  5911  oprabid  5957  eloprabga  6013  resoprab  6022  eqfnov  6033  eqfnov2  6034  ov6g  6065  funimassov  6077  ovelimab  6078  caovord2  6100  uchoice  6204  releldm2  6252  dfoprab4  6259  xporderlem  6298  poxp  6299  f1od2  6302  mpoxopovel  6308  brtpos2  6318  brtpos0  6319  rntpos  6324  dftpos3  6329  tpostpos  6331  tpossym  6343  tposoprab  6347  tfrcllemres  6429  frecabcl  6466  frecsuclem  6473  erth2  6648  qliftfun  6685  erovlem  6695  ecopovsym  6699  ecopovsymg  6702  th3qlem1  6705  mapdm0  6731  elpmg  6732  elpm2g  6733  map0e  6754  dom2lem  6840  mapsnen  6879  xpdom2  6899  xpf1o  6914  mapen  6916  ssfilem  6945  diffitest  6957  ac6sfi  6968  ss1o0el1o  6983  isoti  7082  cnvti  7094  omp1eomlem  7169  ismkvnex  7230  nninfwlporlemd  7247  netap  7337  2omotaplemap  7340  ltexpi  7421  ordpipqqs  7458  ltexnqq  7492  enq0enq  7515  enq0sym  7516  enq0tr  7518  nqnq0pi  7522  genipv  7593  genprndl  7605  genprndu  7606  genpdisj  7607  genpassl  7608  genpassu  7609  addcomprg  7662  mulcomprg  7664  ltnqpr  7677  ltnqpri  7678  ltexprlemm  7684  ltexprlemdisj  7690  suplocexprlemmu  7802  suplocexprlemdisj  7804  ltsrprg  7831  mulgt0sr  7862  elreal2  7914  ltresr  7923  ltresr2  7924  axprecex  7964  axpre-ltadd  7970  axpre-mulgt0  7971  axpre-mulext  7972  axpre-suploclemres  7985  subcan2  8268  negcon1  8295  negcon2  8296  lt0neg1  8512  lt0neg2  8513  le0neg1  8514  le0neg2  8515  reapirr  8621  reapmul1  8639  reapneg  8641  remulext1  8643  apti  8666  negap0  8674  divmulap2  8720  reclt1  8940  recgt1  8941  suprleubex  8998  addltmul  9245  elznn0  9358  zapne  9417  zltlen  9421  nn0lt10b  9423  nn0lt2  9424  eluz1  9622  raluz  9669  rexuz  9671  qltlen  9731  cnref1o  9742  rpnegap  9778  ltxr  9867  xlt0neg1  9930  xlt0neg2  9931  xle0neg1  9932  xle0neg2  9933  elixx1  9989  elixx3g  9993  elioo2  10013  icc0r  10018  elicc4  10032  elioopnf  10059  elioomnf  10060  iooneg  10080  iccneg  10081  iccshftr  10086  iccshftl  10088  iccdil  10090  icccntr  10092  iccf1o  10096  elfz1  10105  0fz1  10137  fzpr  10169  fzdifsuc  10173  uzsplit  10184  elfzm1b  10190  elfzp12  10191  fznn0  10205  exfzdc  10333  zsupcllemstep  10336  flqeqceilz  10427  zmodid2  10461  expap0  10678  qsqeqor  10759  bernneq  10769  hasheqf1o  10894  hashfacen  10945  sqrtmsq2i  11317  maxclpr  11404  minmax  11412  xrmaxlesup  11441  xrnegiso  11444  xrnegcon1d  11446  xrminmax  11447  clim0  11467  climrecvg1n  11530  summodc  11565  fsumsplit  11589  mertenslem2  11718  prodmodc  11760  fprodsplitdc  11778  fprod2dlemstep  11804  dvdsval2  11972  odd2np1lem  12054  even2n  12056  divalgb  12107  divalgmod  12109  bitsval  12125  bitsmod  12138  gcddvds  12155  bezoutlemmain  12190  nnwofdc  12230  isprm3  12311  prmind2  12313  dvdsprime  12315  coprm  12337  prmdvdsexp  12341  sqrt2irr  12355  sqpweven  12368  2sqpwodd  12369  pythagtriplem2  12460  pythagtrip  12477  pceu  12489  pc11  12525  elrest  12948  grpsubeq0  13288  grpsubadd  13290  issubg3  13398  isnsg  13408  eqger  13430  eqglact  13431  eqgid  13432  srgfcl  13605  dvdsrtr  13733  dvdsr02  13737  isunitd  13738  isrhm  13790  isrim0  13793  subsubrng2  13847  subsubrg2  13878  issubrg3  13879  opprdomnbg  13906  2idlelb  14137  istopon  14333  isbasis2g  14365  isbasis3g  14366  tgss2  14399  bastop1  14403  iscld  14423  ntreq0  14452  restsn  14500  restopn2  14503  lmbr  14533  cnptoprest2  14560  txbas  14578  eltx  14579  txlm  14599  ishmeo  14624  hmeoimaf1o  14634  ispsmet  14643  ismet  14664  isxmet  14665  ismet2  14674  metn0  14698  elblps  14710  elbl  14711  bdbl  14823  qtopbasss  14841  elcncf  14893  ellimc3apf  14980  elply  15054  sincosq1sgn  15146  sincosq2sgn  15147  cos11  15173  logrpap0b  15196  lgsdir2lem4  15356  gausslemma2dlem0i  15382  lgsquadlem2  15403  m1lgs  15410  2lgsoddprmlem3  15436  2sqlem6  15445  2sqlem9  15449  2sqlem10  15450  2omap  15726  subctctexmid  15731  iooref1o  15765  iswomni0  15782