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  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  3870  2ralunsn  3922  eluniab  3945  elintab  3979  dfiun2g  4042  dfiin2g  4043  cbvopab1  4202  cbvmpt  4224  axsepg  4248  bnd2  4308  opeqsn  4391  reusv3  4604  tfisi  4732  opeliunxp  4828  eliunxp  4917  relop  4928  eldm2g  4975  reldm0  4997  relrn0  5042  restidsing  5117  xpmlem  5206  elxp5  5274  cnvpom  5328  cbviota  5340  iota1  5350  sniota  5366  fncnv  5445  fnres  5498  brprcneu  5686  fnopfvb  5739  fvelrnb  5747  fvelimab  5756  fvopab3g  5775  eqfnfv3  5802  eqfnfv2f  5804  fvreseq  5806  fnreseql  5813  respreima  5830  rexrn  5839  ralrn  5840  f1ompt  5853  fsn  5874  fconstfvm  5927  fconst3m  5928  fconst4m  5929  foima2  5951  rexima  5954  ralima  5955  dff13  5968  foeqcnvco  5990  fliftfun  5996  isocnv  6011  isoini  6018  f1oiso  6026  cbvriota  6044  riotaeqimp  6057  eusvobj2  6065  oprabid  6111  eloprabga  6169  resoprab  6178  eqfnov  6189  eqfnov2  6190  ov6g  6221  funimassov  6233  ovelimab  6234  caovord2  6256  uchoice  6365  releldm2  6413  dfoprab4  6420  xporderlem  6461  poxp  6462  f1od2  6465  elsuppfng  6476  elsuppfn  6477  rexsupp  6487  mpoxopovel  6506  brtpos2  6516  brtpos0  6517  rntpos  6522  dftpos3  6527  tpostpos  6529  tpossym  6541  tposoprab  6545  tfrcllemres  6627  frecabcl  6664  frecsuclem  6671  erth2  6848  qliftfun  6885  erovlem  6895  ecopovsym  6899  ecopovsymg  6902  th3qlem1  6905  mapdm0  6931  elpmg  6932  elpm2g  6933  map0e  6961  dom2lem  7052  mapsnend  7093  mapsnen  7094  xpdom2  7123  xpf1o  7138  mapen  7140  ssfilem  7171  ssfilemd  7173  diffitest  7185  ac6sfi  7196  eqsndc  7204  ss1o0el1o  7214  2omap  7312  isoti  7341  cnvti  7353  omp1eomlem  7428  ismkvnex  7489  nninfwlporlemd  7506  en2prde  7533  netap  7614  2omotaplemap  7617  ltexpi  7698  ordpipqqs  7735  ltexnqq  7769  enq0enq  7792  enq0sym  7793  enq0tr  7795  nqnq0pi  7799  genipv  7870  genprndl  7882  genprndu  7883  genpdisj  7884  genpassl  7885  genpassu  7886  addcomprg  7939  mulcomprg  7941  ltnqpr  7954  ltnqpri  7955  ltexprlemm  7961  ltexprlemdisj  7967  suplocexprlemmu  8079  suplocexprlemdisj  8081  ltsrprg  8108  mulgt0sr  8139  elreal2  8191  ltresr  8200  ltresr2  8201  axprecex  8241  axpre-ltadd  8247  axpre-mulgt0  8248  axpre-mulext  8249  axpre-suploclemres  8262  subcan2  8545  negcon1  8572  negcon2  8573  lt0neg1  8790  lt0neg2  8791  le0neg1  8792  le0neg2  8793  reapirr  8899  reapmul1  8917  reapneg  8919  remulext1  8921  apti  8944  negap0  8952  divmulap2  9000  reclt1  9220  recgt1  9221  suprleubex  9278  addltmul  9525  elznn0  9642  zapne  9702  zltlen  9707  nn0lt10b  9709  nn0lt2  9710  eluz1  9908  raluz  9961  rexuz  9963  qltlen  10023  cnref1o  10034  rpnegap  10070  ltxr  10160  xlt0neg1  10223  xlt0neg2  10224  xle0neg1  10225  xle0neg2  10226  elixx1  10282  elixx3g  10286  elioo2  10306  icc0r  10311  elicc4  10325  elioopnf  10352  elioomnf  10353  iooneg  10373  iccneg  10374  iccshftr  10379  iccshftl  10381  iccdil  10383  icccntr  10385  iccf1o  10390  elfz1  10399  0fz1  10432  fzpr  10467  fzdifsuc  10471  uzsplit  10482  elfzm1b  10488  elfzp12  10489  fznn0  10503  exfzdc  10642  zsupcllemstep  10645  flqeqceilz  10738  zmodid2  10772  expap0  10989  qsqeqor  11070  bernneq  11081  hasheqf1o  11207  ssenneg  11263  hashfibclem  11265  hashfacen  11267  hashf1  11270  ccatrn  11360  pfxsuffeqwrdeq  11453  wrd2ind  11478  sqrtmsq2i  11884  maxclpr  11971  minmax  11979  xrmaxlesup  12008  xrnegiso  12011  xrnegcon1d  12013  xrminmax  12014  clim0  12034  climrecvg1n  12097  summodc  12133  fsumsplit  12157  mertenslem2  12286  prodmodc  12328  fprodsplitdc  12346  fprod2dlemstep  12372  dvdsval2  12540  odd2np1lem  12622  even2n  12624  divalgb  12675  divalgmod  12677  bitsval  12693  bitsmod  12706  gcddvds  12723  bezoutlemmain  12758  nnwofdc  12798  isprm3  12879  prmind2  12881  dvdsprime  12883  coprm  12905  prmdvdsexp  12909  sqrt2irr  12923  sqpweven  12936  2sqpwodd  12937  pythagtriplem2  13028  pythagtrip  13045  pceu  13057  pc11  13093  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemodife  13223  elrest  13583  grpsubeq0  13874  grpsubadd  13876  issubg3  13978  isnsg  13988  eqger  14010  eqglact  14011  eqgid  14012  srgfcl  14260  dvdsrtr  14391  dvdsr02  14395  isunitd  14396  isrhm  14448  isrim0  14451  subsubrng2  14506  subsubrg2  14537  issubrg3  14538  opprdomnbg  14566  2idlelb  14825  mplelbascoe  15066  istopon  15097  isbasis2g  15129  isbasis3g  15130  tgss2  15163  bastop1  15167  iscld  15187  ntreq0  15216  restsn  15264  restopn2  15267  lmbr  15297  cnptoprest2  15324  txbas  15342  eltx  15343  txlm  15363  ishmeo  15388  hmeoimaf1o  15398  ispsmet  15407  ismet  15428  isxmet  15429  ismet2  15438  metn0  15462  elblps  15474  elbl  15475  bdbl  15587  qtopbasss  15605  elcncf  15657  ellimc3apf  15744  elply  15818  sincosq1sgn  15910  sincosq2sgn  15911  cos11  15937  logrpap0b  15960  lgsdir2lem4  16133  gausslemma2dlem0i  16159  lgsquadlem2  16180  m1lgs  16187  2lgsoddprmlem3  16213  2sqlem6  16222  2sqlem9  16226  2sqlem10  16227  vtxdfifiun  16521  wlkl1loop  16582  wlkv0  16593  wlklenvclwlk  16597  upgr2wlkdc  16601  isclwwlk  16618  isclwwlkng  16630  isclwwlknx  16640  clwwlkn2  16645  eupth2lem2dc  16683  eupth2lem3lem6fi  16695  pw1map  17008  subctctexmid  17013  iooref1o  17057  iswomni0  17075