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  4205  cbvmpt  4228  axsepg  4252  bnd2  4312  opeqsn  4395  reusv3  4608  tfisi  4736  opeliunxp  4832  eliunxp  4921  relop  4932  eldm2g  4979  reldm0  5001  relrn0  5046  restidsing  5122  xpmlem  5211  elxp5  5279  cnvpom  5333  cbviota  5345  iota1  5355  sniota  5371  fncnv  5450  fnres  5503  brprcneu  5691  fnopfvb  5745  fvelrnb  5753  fvelimab  5762  fvopab3g  5781  eqfnfv3  5811  eqfnfv2f  5813  fvreseq  5815  fnreseql  5822  respreima  5839  rexrn  5848  ralrn  5849  f1ompt  5862  fsn  5883  fconstfvm  5936  fconst3m  5937  fconst4m  5938  foima2  5960  rexima  5963  ralima  5964  dff13  5977  foeqcnvco  5999  fliftfun  6005  isocnv  6020  isoini  6027  f1oiso  6035  cbvriota  6053  riotaeqimp  6066  eusvobj2  6074  oprabid  6120  eloprabga  6178  resoprab  6187  eqfnov  6198  eqfnov2  6199  ov6g  6230  funimassov  6242  ovelimab  6243  caovord2  6265  uchoice  6375  releldm2  6423  dfoprab4  6430  xporderlem  6471  poxp  6472  f1od2  6475  elsuppfng  6486  elsuppfn  6487  rexsupp  6497  mpoxopovel  6516  brtpos2  6526  brtpos0  6527  rntpos  6532  dftpos3  6537  tpostpos  6539  tpossym  6551  tposoprab  6555  tfrcllemres  6637  frecabcl  6674  frecsuclem  6681  erth2  6858  qliftfun  6895  erovlem  6905  ecopovsym  6909  ecopovsymg  6912  th3qlem1  6915  mapdm0  6941  elpmg  6942  elpm2g  6943  map0e  6971  dom2lem  7062  mapsnend  7103  mapsnen  7104  xpdom2  7133  xpf1o  7148  mapen  7150  ssfilem  7181  ssfilemd  7183  diffitest  7195  ac6sfi  7206  eqsndc  7214  ss1o0el1o  7224  2omap  7324  isoti  7353  cnvti  7365  omp1eomlem  7440  ismkvnex  7501  nninfwlporlemd  7518  en2prde  7545  netap  7626  2omotaplemap  7629  ltexpi  7710  ordpipqqs  7747  ltexnqq  7781  enq0enq  7804  enq0sym  7805  enq0tr  7807  nqnq0pi  7811  genipv  7882  genprndl  7894  genprndu  7895  genpdisj  7896  genpassl  7897  genpassu  7898  addcomprg  7951  mulcomprg  7953  ltnqpr  7966  ltnqpri  7967  ltexprlemm  7973  ltexprlemdisj  7979  suplocexprlemmu  8091  suplocexprlemdisj  8093  ltsrprg  8120  mulgt0sr  8151  elreal2  8203  ltresr  8212  ltresr2  8213  axprecex  8253  axpre-ltadd  8259  axpre-mulgt0  8260  axpre-mulext  8261  axpre-suploclemres  8274  subcan2  8558  negcon1  8585  negcon2  8586  lt0neg1  8803  lt0neg2  8804  le0neg1  8805  le0neg2  8806  reapirr  8913  reapmul1  8931  reapneg  8933  remulext1  8935  apti  8958  negap0  8966  divmulap2  9014  reclt1  9234  recgt1  9235  suprleubex  9292  addltmul  9553  elznn0  9670  zapne  9730  zltlen  9735  nn0lt10b  9737  nn0lt2  9738  eluz1  9941  raluz  9994  rexuz  9996  qltlen  10056  cnref1o  10068  rpnegap  10104  ltxr  10194  xlt0neg1  10257  xlt0neg2  10258  xle0neg1  10259  xle0neg2  10260  elixx1  10316  elixx3g  10320  elioo2  10340  icc0r  10345  elicc4  10359  elioopnf  10386  elioomnf  10387  iooneg  10407  iccneg  10408  iccshftr  10413  iccshftl  10415  iccdil  10417  icccntr  10419  iccf1o  10424  elfz1  10433  0fz1  10466  fzpr  10501  fzdifsuc  10505  uzsplit  10516  elfzm1b  10522  elfzp12  10523  fznn0  10537  exfzdc  10676  zsupcllemstep  10679  flqeqceilz  10776  zmodid2  10810  expap0  11027  qsqeqor  11108  bernneq  11119  hasheqf1o  11246  ssenneg  11302  hashfibclem  11304  hashfacen  11306  hashf1  11309  ccatrn  11399  pfxsuffeqwrdeq  11492  wrd2ind  11517  sqrtmsq2i  11924  maxclpr  12011  minmax  12020  xrmaxlesup  12050  xrnegiso  12053  xrnegcon1d  12055  xrminmax  12056  clim0  12076  climrecvg1n  12139  summodc  12175  fsumsplit  12199  mertenslem2  12328  prodmodc  12370  fprodsplitdc  12388  fprod2dlemstep  12414  dvdsval2  12582  odd2np1lem  12664  even2n  12666  divalgb  12717  divalgmod  12719  bitsval  12735  bitsmod  12748  gcddvds  12765  bezoutlemmain  12800  nnwofdc  12840  isprm3  12921  prmind2  12923  dvdsprime  12925  coprm  12948  prmdvdsexp  12952  sqrt2irr  12966  sqpweven  12980  2sqpwodd  12981  pythagtriplem2  13074  pythagtrip  13091  pceu  13103  pc11  13139  prmlem0  13249  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemodife  13298  elrest  13659  grpsubeq0  13950  grpsubadd  13952  issubg3  14054  isnsg  14064  eqger  14086  eqglact  14087  eqgid  14088  elcntz  14154  elcntzsn  14157  sscntz  14158  idjusnfi  14270  srgfcl  14384  dvdsrtr  14517  dvdsr02  14521  isunitd  14522  isrhm  14574  isrim0  14577  subsubrng2  14632  subsubrg2  14663  issubrg3  14664  opprdomnbg  14692  2idlelb  14951  mplelbascoe  15208  istopon  15239  isbasis2g  15271  isbasis3g  15272  tgss2  15305  bastop1  15309  iscld  15329  ntreq0  15358  restsn  15406  restopn2  15409  lmbr  15439  cnptoprest2  15466  txbas  15484  eltx  15485  txlm  15505  ishmeo  15530  hmeoimaf1o  15540  ispsmet  15549  ismet  15570  isxmet  15571  ismet2  15580  metn0  15604  elblps  15616  elbl  15617  bdbl  15729  qtopbasss  15747  elcncf  15799  ellimc3apf  15886  elply  15960  efap1p  16005  sincosq1sgn  16053  sincosq2sgn  16054  cos11  16081  logrpap0b  16106  lgsdir2lem4  16355  gausslemma2dlem0i  16381  lgsquadlem2  16402  m1lgs  16409  2lgsoddprmlem3  16435  2sqlem6  16444  2sqlem9  16448  2sqlem10  16449  vtxdfifiun  16743  wlkl1loop  16804  wlkv0  16815  wlklenvclwlk  16819  upgr2wlkdc  16823  isclwwlk  16840  isclwwlkng  16852  isclwwlknx  16862  clwwlkn2  16867  eupth2lem2dc  16905  eupth2lem3lem6fi  16917  pw1map  17230  subctctexmid  17235  iooref1o  17289  iswomni0  17308