Theorem bitrdi 196

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitrdi.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitrdi.2	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
bitrdi	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitrdi

Step	Hyp	Ref	Expression
1		bitrdi.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitrdi.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	2	a1i 9	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 188	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

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  893  pm5.75  968  xordidc  1441  19.17  1602  alexdc  1665  nf4dc  1716  abeq2d  2342  cbvralf  2756  cbvrexf  2757  cbvreu  2763  cbvrab  2797  ceqsralt  2827  ralab2  2967  rexab2  2969  euxfr2dc  2988  reu7  2998  reu8  2999  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  ralss  3290  rexss  3291  elif  3614  prssg  3825  2ralunsn  3877  eluniab  3900  elintab  3934  dfiun2g  3997  dfiin2g  3998  cbvopab1  4157  cbvmpt  4179  axsep2  4203  bnd2  4257  opeqsn  4339  reusv3  4551  tfisi  4679  opeliunxp  4774  eliunxp  4861  relop  4872  eldm2g  4919  reldm0  4941  relrn0  4986  restidsing  5061  xpmlem  5149  elxp5  5217  cnvpom  5271  cbviota  5283  iota1  5293  sniota  5309  fncnv  5387  fnres  5440  brprcneu  5622  fnopfvb  5675  fvelrnb  5683  fvelimab  5692  fvopab3g  5709  eqfnfv3  5736  eqfnfv2f  5738  fvreseq  5740  fnreseql  5747  rexsupp  5761  respreima  5765  rexrn  5774  ralrn  5775  f1ompt  5788  fsn  5809  fconstfvm  5861  fconst3m  5862  fconst4m  5863  foima2  5881  rexima  5884  ralima  5885  dff13  5898  foeqcnvco  5920  fliftfun  5926  isocnv  5941  isoini  5948  f1oiso  5956  cbvriota  5972  riotaeqimp  5985  eusvobj2  5993  oprabid  6039  eloprabga  6097  resoprab  6106  eqfnov  6117  eqfnov2  6118  ov6g  6149  funimassov  6161  ovelimab  6162  caovord2  6184  uchoice  6289  releldm2  6337  dfoprab4  6344  xporderlem  6383  poxp  6384  f1od2  6387  mpoxopovel  6393  brtpos2  6403  brtpos0  6404  rntpos  6409  dftpos3  6414  tpostpos  6416  tpossym  6428  tposoprab  6432  tfrcllemres  6514  frecabcl  6551  frecsuclem  6558  erth2  6735  qliftfun  6772  erovlem  6782  ecopovsym  6786  ecopovsymg  6789  th3qlem1  6792  mapdm0  6818  elpmg  6819  elpm2g  6820  map0e  6841  dom2lem  6931  mapsnen  6972  xpdom2  6998  xpf1o  7013  mapen  7015  ssfilem  7045  diffitest  7057  ac6sfi  7068  ss1o0el1o  7083  isoti  7182  cnvti  7194  omp1eomlem  7269  ismkvnex  7330  nninfwlporlemd  7347  en2prde  7374  netap  7448  2omotaplemap  7451  ltexpi  7532  ordpipqqs  7569  ltexnqq  7603  enq0enq  7626  enq0sym  7627  enq0tr  7629  nqnq0pi  7633  genipv  7704  genprndl  7716  genprndu  7717  genpdisj  7718  genpassl  7719  genpassu  7720  addcomprg  7773  mulcomprg  7775  ltnqpr  7788  ltnqpri  7789  ltexprlemm  7795  ltexprlemdisj  7801  suplocexprlemmu  7913  suplocexprlemdisj  7915  ltsrprg  7942  mulgt0sr  7973  elreal2  8025  ltresr  8034  ltresr2  8035  axprecex  8075  axpre-ltadd  8081  axpre-mulgt0  8082  axpre-mulext  8083  axpre-suploclemres  8096  subcan2  8379  negcon1  8406  negcon2  8407  lt0neg1  8623  lt0neg2  8624  le0neg1  8625  le0neg2  8626  reapirr  8732  reapmul1  8750  reapneg  8752  remulext1  8754  apti  8777  negap0  8785  divmulap2  8831  reclt1  9051  recgt1  9052  suprleubex  9109  addltmul  9356  elznn0  9469  zapne  9529  zltlen  9533  nn0lt10b  9535  nn0lt2  9536  eluz1  9734  raluz  9781  rexuz  9783  qltlen  9843  cnref1o  9854  rpnegap  9890  ltxr  9979  xlt0neg1  10042  xlt0neg2  10043  xle0neg1  10044  xle0neg2  10045  elixx1  10101  elixx3g  10105  elioo2  10125  icc0r  10130  elicc4  10144  elioopnf  10171  elioomnf  10172  iooneg  10192  iccneg  10193  iccshftr  10198  iccshftl  10200  iccdil  10202  icccntr  10204  iccf1o  10208  elfz1  10217  0fz1  10249  fzpr  10281  fzdifsuc  10285  uzsplit  10296  elfzm1b  10302  elfzp12  10303  fznn0  10317  exfzdc  10454  zsupcllemstep  10457  flqeqceilz  10548  zmodid2  10582  expap0  10799  qsqeqor  10880  bernneq  10890  hasheqf1o  11015  hashfacen  11066  ccatrn  11152  pfxsuffeqwrdeq  11238  wrd2ind  11263  sqrtmsq2i  11654  maxclpr  11741  minmax  11749  xrmaxlesup  11778  xrnegiso  11781  xrnegcon1d  11783  xrminmax  11784  clim0  11804  climrecvg1n  11867  summodc  11902  fsumsplit  11926  mertenslem2  12055  prodmodc  12097  fprodsplitdc  12115  fprod2dlemstep  12141  dvdsval2  12309  odd2np1lem  12391  even2n  12393  divalgb  12444  divalgmod  12446  bitsval  12462  bitsmod  12475  gcddvds  12492  bezoutlemmain  12527  nnwofdc  12567  isprm3  12648  prmind2  12650  dvdsprime  12652  coprm  12674  prmdvdsexp  12678  sqrt2irr  12692  sqpweven  12705  2sqpwodd  12706  pythagtriplem2  12797  pythagtrip  12814  pceu  12826  pc11  12862  elrest  13287  grpsubeq0  13627  grpsubadd  13629  issubg3  13737  isnsg  13747  eqger  13769  eqglact  13770  eqgid  13771  srgfcl  13944  dvdsrtr  14073  dvdsr02  14077  isunitd  14078  isrhm  14130  isrim0  14133  subsubrng2  14187  subsubrg2  14218  issubrg3  14219  opprdomnbg  14246  2idlelb  14477  mplelbascoe  14664  istopon  14695  isbasis2g  14727  isbasis3g  14728  tgss2  14761  bastop1  14765  iscld  14785  ntreq0  14814  restsn  14862  restopn2  14865  lmbr  14895  cnptoprest2  14922  txbas  14940  eltx  14941  txlm  14961  ishmeo  14986  hmeoimaf1o  14996  ispsmet  15005  ismet  15026  isxmet  15027  ismet2  15036  metn0  15060  elblps  15072  elbl  15073  bdbl  15185  qtopbasss  15203  elcncf  15255  ellimc3apf  15342  elply  15416  sincosq1sgn  15508  sincosq2sgn  15509  cos11  15535  logrpap0b  15558  lgsdir2lem4  15718  gausslemma2dlem0i  15744  lgsquadlem2  15765  m1lgs  15772  2lgsoddprmlem3  15798  2sqlem6  15807  2sqlem9  15811  2sqlem10  15812  wlkl1loop  16079  wlkv0  16090  wlklenvclwlk  16094  upgr2wlkdc  16096  2omap  16388  pw1map  16390  subctctexmid  16395  iooref1o  16432  iswomni0  16449