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  896  pm5.75  971  xordidc  1444  19.17  1605  alexdc  1668  nf4dc  1718  abeq2d  2344  cbvralf  2759  cbvrexf  2760  cbvreu  2766  cbvrab  2801  ceqsralt  2831  ralab2  2971  rexab2  2973  euxfr2dc  2992  reu7  3002  reu8  3003  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  ralss  3294  rexss  3295  elif  3621  prssg  3835  2ralunsn  3887  eluniab  3910  elintab  3944  dfiun2g  4007  dfiin2g  4008  cbvopab1  4167  cbvmpt  4189  axsep2  4213  bnd2  4269  opeqsn  4351  reusv3  4563  tfisi  4691  opeliunxp  4787  eliunxp  4875  relop  4886  eldm2g  4933  reldm0  4955  relrn0  5000  restidsing  5075  xpmlem  5164  elxp5  5232  cnvpom  5286  cbviota  5298  iota1  5308  sniota  5324  fncnv  5403  fnres  5456  brprcneu  5641  fnopfvb  5694  fvelrnb  5702  fvelimab  5711  fvopab3g  5728  eqfnfv3  5755  eqfnfv2f  5757  fvreseq  5759  fnreseql  5766  respreima  5783  rexrn  5792  ralrn  5793  f1ompt  5806  fsn  5827  fconstfvm  5880  fconst3m  5881  fconst4m  5882  foima2  5902  rexima  5905  ralima  5906  dff13  5919  foeqcnvco  5941  fliftfun  5947  isocnv  5962  isoini  5969  f1oiso  5977  cbvriota  5993  riotaeqimp  6006  eusvobj2  6014  oprabid  6060  eloprabga  6118  resoprab  6127  eqfnov  6138  eqfnov2  6139  ov6g  6170  funimassov  6182  ovelimab  6183  caovord2  6205  uchoice  6309  releldm2  6357  dfoprab4  6364  xporderlem  6405  poxp  6406  f1od2  6409  elsuppfng  6420  elsuppfn  6421  rexsupp  6431  mpoxopovel  6450  brtpos2  6460  brtpos0  6461  rntpos  6466  dftpos3  6471  tpostpos  6473  tpossym  6485  tposoprab  6489  tfrcllemres  6571  frecabcl  6608  frecsuclem  6615  erth2  6792  qliftfun  6829  erovlem  6839  ecopovsym  6843  ecopovsymg  6846  th3qlem1  6849  mapdm0  6875  elpmg  6876  elpm2g  6877  map0e  6898  dom2lem  6988  mapsnen  7029  xpdom2  7058  xpf1o  7073  mapen  7075  ssfilem  7105  ssfilemd  7107  diffitest  7119  ac6sfi  7130  eqsndc  7138  ss1o0el1o  7148  isoti  7249  cnvti  7261  omp1eomlem  7336  ismkvnex  7397  nninfwlporlemd  7414  en2prde  7441  netap  7516  2omotaplemap  7519  ltexpi  7600  ordpipqqs  7637  ltexnqq  7671  enq0enq  7694  enq0sym  7695  enq0tr  7697  nqnq0pi  7701  genipv  7772  genprndl  7784  genprndu  7785  genpdisj  7786  genpassl  7787  genpassu  7788  addcomprg  7841  mulcomprg  7843  ltnqpr  7856  ltnqpri  7857  ltexprlemm  7863  ltexprlemdisj  7869  suplocexprlemmu  7981  suplocexprlemdisj  7983  ltsrprg  8010  mulgt0sr  8041  elreal2  8093  ltresr  8102  ltresr2  8103  axprecex  8143  axpre-ltadd  8149  axpre-mulgt0  8150  axpre-mulext  8151  axpre-suploclemres  8164  subcan2  8446  negcon1  8473  negcon2  8474  lt0neg1  8690  lt0neg2  8691  le0neg1  8692  le0neg2  8693  reapirr  8799  reapmul1  8817  reapneg  8819  remulext1  8821  apti  8844  negap0  8852  divmulap2  8898  reclt1  9118  recgt1  9119  suprleubex  9176  addltmul  9423  elznn0  9538  zapne  9598  zltlen  9602  nn0lt10b  9604  nn0lt2  9605  eluz1  9803  raluz  9856  rexuz  9858  qltlen  9918  cnref1o  9929  rpnegap  9965  ltxr  10054  xlt0neg1  10117  xlt0neg2  10118  xle0neg1  10119  xle0neg2  10120  elixx1  10176  elixx3g  10180  elioo2  10200  icc0r  10205  elicc4  10219  elioopnf  10246  elioomnf  10247  iooneg  10267  iccneg  10268  iccshftr  10273  iccshftl  10275  iccdil  10277  icccntr  10279  iccf1o  10284  elfz1  10293  0fz1  10325  fzpr  10357  fzdifsuc  10361  uzsplit  10372  elfzm1b  10378  elfzp12  10379  fznn0  10393  exfzdc  10532  zsupcllemstep  10535  flqeqceilz  10626  zmodid2  10660  expap0  10877  qsqeqor  10958  bernneq  10968  hasheqf1o  11093  hashfacen  11146  ccatrn  11235  pfxsuffeqwrdeq  11328  wrd2ind  11353  sqrtmsq2i  11758  maxclpr  11845  minmax  11853  xrmaxlesup  11882  xrnegiso  11885  xrnegcon1d  11887  xrminmax  11888  clim0  11908  climrecvg1n  11971  summodc  12007  fsumsplit  12031  mertenslem2  12160  prodmodc  12202  fprodsplitdc  12220  fprod2dlemstep  12246  dvdsval2  12414  odd2np1lem  12496  even2n  12498  divalgb  12549  divalgmod  12551  bitsval  12567  bitsmod  12580  gcddvds  12597  bezoutlemmain  12632  nnwofdc  12672  isprm3  12753  prmind2  12755  dvdsprime  12757  coprm  12779  prmdvdsexp  12783  sqrt2irr  12797  sqpweven  12810  2sqpwodd  12811  pythagtriplem2  12902  pythagtrip  12919  pceu  12931  pc11  12967  elrest  13392  grpsubeq0  13732  grpsubadd  13734  issubg3  13842  isnsg  13852  eqger  13874  eqglact  13875  eqgid  13876  srgfcl  14050  dvdsrtr  14179  dvdsr02  14183  isunitd  14184  isrhm  14236  isrim0  14239  subsubrng2  14293  subsubrg2  14324  issubrg3  14325  opprdomnbg  14353  2idlelb  14584  mplelbascoe  14776  istopon  14807  isbasis2g  14839  isbasis3g  14840  tgss2  14873  bastop1  14877  iscld  14897  ntreq0  14926  restsn  14974  restopn2  14977  lmbr  15007  cnptoprest2  15034  txbas  15052  eltx  15053  txlm  15073  ishmeo  15098  hmeoimaf1o  15108  ispsmet  15117  ismet  15138  isxmet  15139  ismet2  15148  metn0  15172  elblps  15184  elbl  15185  bdbl  15297  qtopbasss  15315  elcncf  15367  ellimc3apf  15454  elply  15528  sincosq1sgn  15620  sincosq2sgn  15621  cos11  15647  logrpap0b  15670  lgsdir2lem4  15833  gausslemma2dlem0i  15859  lgsquadlem2  15880  m1lgs  15887  2lgsoddprmlem3  15913  2sqlem6  15922  2sqlem9  15926  2sqlem10  15927  vtxdfifiun  16221  wlkl1loop  16282  wlkv0  16293  wlklenvclwlk  16297  upgr2wlkdc  16301  isclwwlk  16318  isclwwlkng  16330  isclwwlknx  16340  clwwlkn2  16345  eupth2lem2dc  16383  eupth2lem3lem6fi  16395  2omap  16698  pw1map  16700  subctctexmid  16705  iooref1o  16749  iswomni0  16767