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  883  pm5.75  957  xordidc  1394  19.17  1549  alexdc  1612  nf4dc  1663  abeq2d  2283  cbvralf  2689  cbvrexf  2690  cbvreu  2694  cbvrab  2728  ceqsralt  2757  ralab2  2894  rexab2  2896  euxfr2dc  2915  reu7  2925  reu8  2926  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  ralss  3213  rexss  3214  prssg  3737  2ralunsn  3785  eluniab  3808  elintab  3842  dfiun2g  3905  dfiin2g  3906  cbvopab1  4062  cbvmpt  4084  axsep2  4108  bnd2  4159  opeqsn  4237  reusv3  4445  tfisi  4571  opeliunxp  4666  eliunxp  4750  relop  4761  eldm2g  4807  reldm0  4829  relrn0  4873  xpmlem  5031  elxp5  5099  cnvpom  5153  cbviota  5165  iota1  5174  sniota  5189  fncnv  5264  fnres  5314  brprcneu  5489  fnopfvb  5538  fvelrnb  5544  fvelimab  5552  fvopab3g  5569  eqfnfv3  5595  eqfnfv2f  5597  fvreseq  5599  fnreseql  5606  rexsupp  5620  respreima  5624  rexrn  5633  ralrn  5634  f1ompt  5647  fsn  5668  fconstfvm  5714  fconst3m  5715  fconst4m  5716  foima2  5731  rexima  5734  ralima  5735  dff13  5747  foeqcnvco  5769  fliftfun  5775  isocnv  5790  isoini  5797  f1oiso  5805  cbvriota  5819  eusvobj2  5839  oprabid  5885  eloprabga  5940  resoprab  5949  eqfnov  5959  eqfnov2  5960  ov6g  5990  funimassov  6002  ovelimab  6003  caovord2  6025  releldm2  6164  dfoprab4  6171  xporderlem  6210  poxp  6211  f1od2  6214  mpoxopovel  6220  brtpos2  6230  brtpos0  6231  rntpos  6236  dftpos3  6241  tpostpos  6243  tpossym  6255  tposoprab  6259  tfrcllemres  6341  frecabcl  6378  frecsuclem  6385  erth2  6558  qliftfun  6595  erovlem  6605  ecopovsym  6609  ecopovsymg  6612  th3qlem1  6615  mapdm0  6641  elpmg  6642  elpm2g  6643  map0e  6664  dom2lem  6750  mapsnen  6789  xpdom2  6809  xpf1o  6822  mapen  6824  ssfilem  6853  diffitest  6865  ac6sfi  6876  ss1o0el1o  6890  isoti  6984  cnvti  6996  omp1eomlem  7071  ismkvnex  7131  nninfwlporlemd  7148  ltexpi  7299  ordpipqqs  7336  ltexnqq  7370  enq0enq  7393  enq0sym  7394  enq0tr  7396  nqnq0pi  7400  genipv  7471  genprndl  7483  genprndu  7484  genpdisj  7485  genpassl  7486  genpassu  7487  addcomprg  7540  mulcomprg  7542  ltnqpr  7555  ltnqpri  7556  ltexprlemm  7562  ltexprlemdisj  7568  suplocexprlemmu  7680  suplocexprlemdisj  7682  ltsrprg  7709  mulgt0sr  7740  elreal2  7792  ltresr  7801  ltresr2  7802  axprecex  7842  axpre-ltadd  7848  axpre-mulgt0  7849  axpre-mulext  7850  axpre-suploclemres  7863  subcan2  8144  negcon1  8171  negcon2  8172  lt0neg1  8387  lt0neg2  8388  le0neg1  8389  le0neg2  8390  reapirr  8496  reapmul1  8514  reapneg  8516  remulext1  8518  apti  8541  negap0  8549  divmulap2  8593  reclt1  8812  recgt1  8813  suprleubex  8870  addltmul  9114  elznn0  9227  zapne  9286  zltlen  9290  nn0lt10b  9292  nn0lt2  9293  eluz1  9491  raluz  9537  rexuz  9539  qltlen  9599  cnref1o  9609  rpnegap  9643  ltxr  9732  xlt0neg1  9795  xlt0neg2  9796  xle0neg1  9797  xle0neg2  9798  elixx1  9854  elixx3g  9858  elioo2  9878  icc0r  9883  elicc4  9897  elioopnf  9924  elioomnf  9925  iooneg  9945  iccneg  9946  iccshftr  9951  iccshftl  9953  iccdil  9955  icccntr  9957  iccf1o  9961  elfz1  9970  0fz1  10001  fzpr  10033  fzdifsuc  10037  uzsplit  10048  elfzm1b  10054  elfzp12  10055  fznn0  10069  exfzdc  10196  flqeqceilz  10274  zmodid2  10308  expap0  10506  qsqeqor  10586  bernneq  10596  hasheqf1o  10719  hashfacen  10771  sqrtmsq2i  11099  maxclpr  11186  minmax  11193  xrmaxlesup  11222  xrnegiso  11225  xrnegcon1d  11227  xrminmax  11228  clim0  11248  climrecvg1n  11311  summodc  11346  fsumsplit  11370  mertenslem2  11499  prodmodc  11541  fprodsplitdc  11559  fprod2dlemstep  11585  dvdsval2  11752  odd2np1lem  11831  even2n  11833  divalgb  11884  divalgmod  11886  zsupcllemstep  11900  gcddvds  11918  bezoutlemmain  11953  nnwofdc  11993  isprm3  12072  prmind2  12074  dvdsprime  12076  coprm  12098  prmdvdsexp  12102  sqrt2irr  12116  sqpweven  12129  2sqpwodd  12130  pythagtriplem2  12220  pythagtrip  12237  pceu  12249  pc11  12284  elrest  12586  istopon  12805  isbasis2g  12837  isbasis3g  12838  tgss2  12873  bastop1  12877  iscld  12897  ntreq0  12926  restsn  12974  restopn2  12977  lmbr  13007  cnptoprest2  13034  txbas  13052  eltx  13053  txlm  13073  ishmeo  13098  hmeoimaf1o  13108  ispsmet  13117  ismet  13138  isxmet  13139  ismet2  13148  metn0  13172  elblps  13184  elbl  13185  bdbl  13297  qtopbasss  13315  elcncf  13354  ellimc3apf  13423  sincosq1sgn  13541  sincosq2sgn  13542  cos11  13568  logrpap0b  13591  lgsdir2lem4  13726  2sqlem6  13750  2sqlem9  13754  2sqlem10  13755  subctctexmid  14034  iooref1o  14066  iswomni0  14083