Theorem bitrdi 195

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 187	1 |- ( ph -> ( ps <-> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bitr2di  196  bitr4di  197  3bitr3g  221  bibi2i  226  ibibr  245  biancomd  269  imanst  874  pm5.75  947  xordidc  1381  19.17  1536  alexdc  1599  nf4dc  1650  abeq2d  2270  cbvralf  2674  cbvrexf  2675  cbvreu  2678  cbvrab  2710  ceqsralt  2739  ralab2  2876  rexab2  2878  euxfr2dc  2897  reu7  2907  reu8  2908  cbvralcsf  3093  cbvrexcsf  3094  cbvreucsf  3095  cbvrabcsf  3096  ralss  3194  rexss  3195  prssg  3713  2ralunsn  3761  eluniab  3784  elintab  3818  dfiun2g  3881  dfiin2g  3882  cbvopab1  4037  cbvmpt  4059  axsep2  4083  bnd2  4133  opeqsn  4211  reusv3  4418  tfisi  4544  opeliunxp  4638  eliunxp  4722  relop  4733  eldm2g  4779  reldm0  4801  relrn0  4845  xpmlem  5003  elxp5  5071  cnvpom  5125  cbviota  5137  iota1  5146  sniota  5159  fncnv  5233  fnres  5283  brprcneu  5458  fnopfvb  5507  fvelrnb  5513  fvelimab  5521  fvopab3g  5538  eqfnfv3  5564  eqfnfv2f  5566  fvreseq  5568  fnreseql  5574  rexsupp  5588  respreima  5592  rexrn  5601  ralrn  5602  f1ompt  5615  fsn  5636  fconstfvm  5682  fconst3m  5683  fconst4m  5684  foima2  5697  rexima  5700  ralima  5701  dff13  5713  foeqcnvco  5735  fliftfun  5741  isocnv  5756  isoini  5763  f1oiso  5771  cbvriota  5784  eusvobj2  5804  oprabid  5847  eloprabga  5902  resoprab  5911  eqfnov  5921  eqfnov2  5922  ov6g  5952  funimassov  5964  ovelimab  5965  caovord2  5987  releldm2  6127  dfoprab4  6134  xporderlem  6172  poxp  6173  f1od2  6176  mpoxopovel  6182  brtpos2  6192  brtpos0  6193  rntpos  6198  dftpos3  6203  tpostpos  6205  tpossym  6217  tposoprab  6221  tfrcllemres  6303  frecabcl  6340  frecsuclem  6347  erth2  6518  qliftfun  6555  erovlem  6565  ecopovsym  6569  ecopovsymg  6572  th3qlem1  6575  mapdm0  6601  elpmg  6602  elpm2g  6603  map0e  6624  dom2lem  6710  mapsnen  6749  xpdom2  6769  xpf1o  6782  mapen  6784  ssfilem  6813  diffitest  6825  ac6sfi  6836  ss1o0el1o  6850  isoti  6943  cnvti  6955  omp1eomlem  7028  ismkvnex  7081  ltexpi  7240  ordpipqqs  7277  ltexnqq  7311  enq0enq  7334  enq0sym  7335  enq0tr  7337  nqnq0pi  7341  genipv  7412  genprndl  7424  genprndu  7425  genpdisj  7426  genpassl  7427  genpassu  7428  addcomprg  7481  mulcomprg  7483  ltnqpr  7496  ltnqpri  7497  ltexprlemm  7503  ltexprlemdisj  7509  suplocexprlemmu  7621  suplocexprlemdisj  7623  ltsrprg  7650  mulgt0sr  7681  elreal2  7733  ltresr  7742  ltresr2  7743  axprecex  7783  axpre-ltadd  7789  axpre-mulgt0  7790  axpre-mulext  7791  axpre-suploclemres  7804  subcan2  8083  negcon1  8110  negcon2  8111  lt0neg1  8326  lt0neg2  8327  le0neg1  8328  le0neg2  8329  reapirr  8435  reapmul1  8453  reapneg  8455  remulext1  8457  apti  8480  negap0  8488  divmulap2  8532  reclt1  8750  recgt1  8751  suprleubex  8808  addltmul  9052  elznn0  9165  zapne  9221  zltlen  9225  nn0lt10b  9227  nn0lt2  9228  eluz1  9426  raluz  9472  rexuz  9474  qltlen  9531  cnref1o  9541  rpnegap  9575  ltxr  9664  xlt0neg1  9724  xlt0neg2  9725  xle0neg1  9726  xle0neg2  9727  elixx1  9783  elixx3g  9787  elioo2  9807  icc0r  9812  elicc4  9826  elioopnf  9853  elioomnf  9854  iooneg  9874  iccneg  9875  iccshftr  9880  iccshftl  9882  iccdil  9884  icccntr  9886  iccf1o  9890  elfz1  9899  0fz1  9929  fzpr  9961  fzdifsuc  9965  uzsplit  9976  elfzm1b  9982  elfzp12  9983  fznn0  9997  exfzdc  10121  flqeqceilz  10199  zmodid2  10233  expap0  10431  bernneq  10520  hasheqf1o  10641  hashfacen  10689  sqrtmsq2i  11017  maxclpr  11104  minmax  11111  xrmaxlesup  11138  xrnegiso  11141  xrnegcon1d  11143  xrminmax  11144  clim0  11164  climrecvg1n  11227  summodc  11262  fsumsplit  11286  mertenslem2  11415  prodmodc  11457  fprodsplitdc  11475  fprod2dlemstep  11501  dvdsval2  11668  odd2np1lem  11744  even2n  11746  divalgb  11797  divalgmod  11799  zsupcllemstep  11813  gcddvds  11827  bezoutlemmain  11862  isprm3  11975  prmind2  11977  dvdsprime  11979  coprm  11998  prmdvdsexp  12002  sqrt2irr  12016  sqpweven  12029  2sqpwodd  12030  elrest  12318  istopon  12371  isbasis2g  12403  isbasis3g  12404  tgss2  12439  bastop1  12443  iscld  12463  ntreq0  12492  restsn  12540  restopn2  12543  lmbr  12573  cnptoprest2  12600  txbas  12618  eltx  12619  txlm  12639  ishmeo  12664  hmeoimaf1o  12674  ispsmet  12683  ismet  12704  isxmet  12705  ismet2  12714  metn0  12738  elblps  12750  elbl  12751  bdbl  12863  qtopbasss  12881  elcncf  12920  ellimc3apf  12989  sincosq1sgn  13107  sincosq2sgn  13108  cos11  13134  logrpap0b  13157  subctctexmid  13534  iooref1o  13568  iswomni0  13585