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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bitr2di  197  bitr4di  198  3bitr3g  222  bibi2i  227  ibibr  246  biancomd  271  imanst  900  pm5.75  975  xordidc  1448  19.17  1609  alexdc  1672  nf4dc  1722  abeq2d  2351  eqabrd  2378  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvrab  2819  ceqsralt  2849  ralab2  2990  rexab2  2992  euxfr2dc  3011  reu7  3021  reu8  3022  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  ralss  3314  rexss  3315  sseq0b  3564  elif  3652  prssg  3872  2ralunsn  3924  eluniab  3947  elintab  3981  dfiun2g  4044  dfiin2g  4045  cbvopab1  4204  cbvmpt  4226  axsepg  4250  bnd2  4310  opeqsn  4393  reusv3  4606  tfisi  4734  opeliunxp  4830  eliunxp  4919  relop  4930  eldm2g  4977  reldm0  4999  relrn0  5044  restidsing  5119  xpmlem  5208  elxp5  5276  cnvpom  5330  cbviota  5342  iota1  5352  sniota  5368  fncnv  5447  fnres  5500  brprcneu  5688  fnopfvb  5742  fvelrnb  5750  fvelimab  5759  fvopab3g  5778  eqfnfv3  5808  eqfnfv2f  5810  fvreseq  5812  fnreseql  5819  respreima  5836  rexrn  5845  ralrn  5846  f1ompt  5859  fsn  5880  fconstfvm  5933  fconst3m  5934  fconst4m  5935  foima2  5957  rexima  5960  ralima  5961  dff13  5974  foeqcnvco  5996  fliftfun  6002  isocnv  6017  isoini  6024  f1oiso  6032  cbvriota  6050  riotaeqimp  6063  eusvobj2  6071  oprabid  6117  eloprabga  6175  resoprab  6184  eqfnov  6195  eqfnov2  6196  ov6g  6227  funimassov  6239  ovelimab  6240  caovord2  6262  uchoice  6371  releldm2  6419  dfoprab4  6426  xporderlem  6467  poxp  6468  f1od2  6471  elsuppfng  6482  elsuppfn  6483  rexsupp  6493  mpoxopovel  6512  brtpos2  6522  brtpos0  6523  rntpos  6528  dftpos3  6533  tpostpos  6535  tpossym  6547  tposoprab  6551  tfrcllemres  6633  frecabcl  6670  frecsuclem  6677  erth2  6854  qliftfun  6891  erovlem  6901  ecopovsym  6905  ecopovsymg  6908  th3qlem1  6911  mapdm0  6937  elpmg  6938  elpm2g  6939  map0e  6967  dom2lem  7058  mapsnend  7099  mapsnen  7100  xpdom2  7129  xpf1o  7144  mapen  7146  ssfilem  7177  ssfilemd  7179  diffitest  7191  ac6sfi  7202  eqsndc  7210  ss1o0el1o  7220  2omap  7319  isoti  7348  cnvti  7360  omp1eomlem  7435  ismkvnex  7496  nninfwlporlemd  7513  en2prde  7540  netap  7621  2omotaplemap  7624  ltexpi  7705  ordpipqqs  7742  ltexnqq  7776  enq0enq  7799  enq0sym  7800  enq0tr  7802  nqnq0pi  7806  genipv  7877  genprndl  7889  genprndu  7890  genpdisj  7891  genpassl  7892  genpassu  7893  addcomprg  7946  mulcomprg  7948  ltnqpr  7961  ltnqpri  7962  ltexprlemm  7968  ltexprlemdisj  7974  suplocexprlemmu  8086  suplocexprlemdisj  8088  ltsrprg  8115  mulgt0sr  8146  elreal2  8198  ltresr  8207  ltresr2  8208  axprecex  8248  axpre-ltadd  8254  axpre-mulgt0  8255  axpre-mulext  8256  axpre-suploclemres  8269  subcan2  8553  negcon1  8580  negcon2  8581  lt0neg1  8798  lt0neg2  8799  le0neg1  8800  le0neg2  8801  reapirr  8908  reapmul1  8926  reapneg  8928  remulext1  8930  apti  8953  negap0  8961  divmulap2  9009  reclt1  9229  recgt1  9230  suprleubex  9287  addltmul  9547  elznn0  9664  zapne  9724  zltlen  9729  nn0lt10b  9731  nn0lt2  9732  eluz1  9935  raluz  9988  rexuz  9990  qltlen  10050  cnref1o  10062  rpnegap  10098  ltxr  10188  xlt0neg1  10251  xlt0neg2  10252  xle0neg1  10253  xle0neg2  10254  elixx1  10310  elixx3g  10314  elioo2  10334  icc0r  10339  elicc4  10353  elioopnf  10380  elioomnf  10381  iooneg  10401  iccneg  10402  iccshftr  10407  iccshftl  10409  iccdil  10411  icccntr  10413  iccf1o  10418  elfz1  10427  0fz1  10460  fzpr  10495  fzdifsuc  10499  uzsplit  10510  elfzm1b  10516  elfzp12  10517  fznn0  10531  exfzdc  10670  zsupcllemstep  10673  flqeqceilz  10770  zmodid2  10804  expap0  11021  qsqeqor  11102  bernneq  11113  hasheqf1o  11240  ssenneg  11296  hashfibclem  11298  hashfacen  11300  hashf1  11303  ccatrn  11393  pfxsuffeqwrdeq  11486  wrd2ind  11511  sqrtmsq2i  11918  maxclpr  12005  minmax  12014  xrmaxlesup  12044  xrnegiso  12047  xrnegcon1d  12049  xrminmax  12050  clim0  12070  climrecvg1n  12133  summodc  12169  fsumsplit  12193  mertenslem2  12322  prodmodc  12364  fprodsplitdc  12382  fprod2dlemstep  12408  dvdsval2  12576  odd2np1lem  12658  even2n  12660  divalgb  12711  divalgmod  12713  bitsval  12729  bitsmod  12742  gcddvds  12759  bezoutlemmain  12794  nnwofdc  12834  isprm3  12915  prmind2  12917  dvdsprime  12919  coprm  12942  prmdvdsexp  12946  sqrt2irr  12960  sqpweven  12974  2sqpwodd  12975  pythagtriplem2  13068  pythagtrip  13085  pceu  13097  pc11  13133  prmlem0  13243  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemodife  13292  elrest  13653  grpsubeq0  13944  grpsubadd  13946  issubg3  14048  isnsg  14058  eqger  14080  eqglact  14081  eqgid  14082  elcntz  14148  elcntzsn  14151  sscntz  14152  srgfcl  14361  dvdsrtr  14492  dvdsr02  14496  isunitd  14497  isrhm  14549  isrim0  14552  subsubrng2  14607  subsubrg2  14638  issubrg3  14639  opprdomnbg  14667  2idlelb  14926  mplelbascoe  15174  istopon  15205  isbasis2g  15237  isbasis3g  15238  tgss2  15271  bastop1  15275  iscld  15295  ntreq0  15324  restsn  15372  restopn2  15375  lmbr  15405  cnptoprest2  15432  txbas  15450  eltx  15451  txlm  15471  ishmeo  15496  hmeoimaf1o  15506  ispsmet  15515  ismet  15536  isxmet  15537  ismet2  15546  metn0  15570  elblps  15582  elbl  15583  bdbl  15695  qtopbasss  15713  elcncf  15765  ellimc3apf  15852  elply  15926  efap1p  15971  sincosq1sgn  16019  sincosq2sgn  16020  cos11  16046  logrpap0b  16070  lgsdir2lem4  16316  gausslemma2dlem0i  16342  lgsquadlem2  16363  m1lgs  16370  2lgsoddprmlem3  16396  2sqlem6  16405  2sqlem9  16409  2sqlem10  16410  vtxdfifiun  16704  wlkl1loop  16765  wlkv0  16776  wlklenvclwlk  16780  upgr2wlkdc  16784  isclwwlk  16801  isclwwlkng  16813  isclwwlknx  16823  clwwlkn2  16828  eupth2lem2dc  16866  eupth2lem3lem6fi  16878  pw1map  17191  subctctexmid  17196  iooref1o  17249  iswomni0  17268