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  4134  opeqsn  4212  reusv3  4420  tfisi  4546  opeliunxp  4641  eliunxp  4725  relop  4736  eldm2g  4782  reldm0  4804  relrn0  4848  xpmlem  5006  elxp5  5074  cnvpom  5128  cbviota  5140  iota1  5149  sniota  5162  fncnv  5236  fnres  5286  brprcneu  5461  fnopfvb  5510  fvelrnb  5516  fvelimab  5524  fvopab3g  5541  eqfnfv3  5567  eqfnfv2f  5569  fvreseq  5571  fnreseql  5577  rexsupp  5591  respreima  5595  rexrn  5604  ralrn  5605  f1ompt  5618  fsn  5639  fconstfvm  5685  fconst3m  5686  fconst4m  5687  foima2  5702  rexima  5705  ralima  5706  dff13  5718  foeqcnvco  5740  fliftfun  5746  isocnv  5761  isoini  5768  f1oiso  5776  cbvriota  5790  eusvobj2  5810  oprabid  5853  eloprabga  5908  resoprab  5917  eqfnov  5927  eqfnov2  5928  ov6g  5958  funimassov  5970  ovelimab  5971  caovord2  5993  releldm2  6133  dfoprab4  6140  xporderlem  6178  poxp  6179  f1od2  6182  mpoxopovel  6188  brtpos2  6198  brtpos0  6199  rntpos  6204  dftpos3  6209  tpostpos  6211  tpossym  6223  tposoprab  6227  tfrcllemres  6309  frecabcl  6346  frecsuclem  6353  erth2  6525  qliftfun  6562  erovlem  6572  ecopovsym  6576  ecopovsymg  6579  th3qlem1  6582  mapdm0  6608  elpmg  6609  elpm2g  6610  map0e  6631  dom2lem  6717  mapsnen  6756  xpdom2  6776  xpf1o  6789  mapen  6791  ssfilem  6820  diffitest  6832  ac6sfi  6843  ss1o0el1o  6857  isoti  6951  cnvti  6963  omp1eomlem  7038  ismkvnex  7098  ltexpi  7257  ordpipqqs  7294  ltexnqq  7328  enq0enq  7351  enq0sym  7352  enq0tr  7354  nqnq0pi  7358  genipv  7429  genprndl  7441  genprndu  7442  genpdisj  7443  genpassl  7444  genpassu  7445  addcomprg  7498  mulcomprg  7500  ltnqpr  7513  ltnqpri  7514  ltexprlemm  7520  ltexprlemdisj  7526  suplocexprlemmu  7638  suplocexprlemdisj  7640  ltsrprg  7667  mulgt0sr  7698  elreal2  7750  ltresr  7759  ltresr2  7760  axprecex  7800  axpre-ltadd  7806  axpre-mulgt0  7807  axpre-mulext  7808  axpre-suploclemres  7821  subcan2  8100  negcon1  8127  negcon2  8128  lt0neg1  8343  lt0neg2  8344  le0neg1  8345  le0neg2  8346  reapirr  8452  reapmul1  8470  reapneg  8472  remulext1  8474  apti  8497  negap0  8505  divmulap2  8549  reclt1  8767  recgt1  8768  suprleubex  8825  addltmul  9069  elznn0  9182  zapne  9238  zltlen  9242  nn0lt10b  9244  nn0lt2  9245  eluz1  9443  raluz  9489  rexuz  9491  qltlen  9549  cnref1o  9559  rpnegap  9593  ltxr  9682  xlt0neg1  9742  xlt0neg2  9743  xle0neg1  9744  xle0neg2  9745  elixx1  9801  elixx3g  9805  elioo2  9825  icc0r  9830  elicc4  9844  elioopnf  9871  elioomnf  9872  iooneg  9892  iccneg  9893  iccshftr  9898  iccshftl  9900  iccdil  9902  icccntr  9904  iccf1o  9908  elfz1  9917  0fz1  9947  fzpr  9979  fzdifsuc  9983  uzsplit  9994  elfzm1b  10000  elfzp12  10001  fznn0  10015  exfzdc  10139  flqeqceilz  10217  zmodid2  10251  expap0  10449  bernneq  10538  hasheqf1o  10659  hashfacen  10707  sqrtmsq2i  11035  maxclpr  11122  minmax  11129  xrmaxlesup  11156  xrnegiso  11159  xrnegcon1d  11161  xrminmax  11162  clim0  11182  climrecvg1n  11245  summodc  11280  fsumsplit  11304  mertenslem2  11433  prodmodc  11475  fprodsplitdc  11493  fprod2dlemstep  11519  dvdsval2  11686  odd2np1lem  11762  even2n  11764  divalgb  11815  divalgmod  11817  zsupcllemstep  11831  gcddvds  11846  bezoutlemmain  11881  isprm3  11994  prmind2  11996  dvdsprime  11998  coprm  12018  prmdvdsexp  12022  sqrt2irr  12036  sqpweven  12049  2sqpwodd  12050  elrest  12358  istopon  12411  isbasis2g  12443  isbasis3g  12444  tgss2  12479  bastop1  12483  iscld  12503  ntreq0  12532  restsn  12580  restopn2  12583  lmbr  12613  cnptoprest2  12640  txbas  12658  eltx  12659  txlm  12679  ishmeo  12704  hmeoimaf1o  12714  ispsmet  12723  ismet  12744  isxmet  12745  ismet2  12754  metn0  12778  elblps  12790  elbl  12791  bdbl  12903  qtopbasss  12921  elcncf  12960  ellimc3apf  13029  sincosq1sgn  13147  sincosq2sgn  13148  cos11  13174  logrpap0b  13197  subctctexmid  13573  iooref1o  13605  iswomni0  13622