Theorem bitr2di 289

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

Hypotheses

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

Assertion

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

Proof of Theorem bitr2di

Step	Hyp	Ref	Expression
1		bitr2di.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitr2di.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	1, 2	bitrdi 288	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	3	bicomd 224	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208

This theorem is referenced by:  bitr4id  291  bibif  372  oranabs  1007  necon4bid  2980  2reu4lem  4458  resopab2  5995  xpco  6247  funconstss  7004  xpopth  7979  xpord2pred  8092  snmapen  8982  ac6sfi  9191  supgtoreq  9381  rankr1bg  9725  alephsdom  10006  brdom7disj  10451  fpwwe2lem12  10563  nn0sub  12485  elznn0  12537  nn01to3  12889  supxrbnd1  13271  supxrbnd2  13272  rexuz3  15309  smueqlem  16457  qnumdenbi  16712  dfiso3  17738  tltnle  18384  lssne0  20948  pjfval2  21691  0top  22973  1stccn  23453  dscopn  24563  bcthlem1  25316  ovolgelb  25472  iblpos  25785  itgposval  25788  itgsubstlem  26040  sincosq3sgn  26489  sincosq4sgn  26490  lgsquadlem3  27370  elzs2  28416  colinearalg  29004  elntg2  29079  wlklnwwlkln2lem  29975  2pthdlem1  30023  wwlks2onsym  30053  rusgrnumwwlkb0  30067  numclwwlk2lem1  30471  nmoo0  30887  leop3  32221  leoptri  32232  f1od2  32818  fedgmullem2  33821  r1ssel  35295  vonf1owev  35343  dfrdg4  36186  mh-regprimbi  36780  curf  37972  poimirlem28  38022  itgaddnclem2  38053  relssinxpdmrn  38723  lfl1dim  39620  glbconxN  39877  2dim  39969  elpadd0  40308  dalawlem13  40382  diclspsn  41693  dihglb2  41841  dochsordN  41873  redvmptabs  42844  lzunuz  43224  tfsconcat0b  43798  uneqsn  44476  ntrclskb  44520  ntrneiel2  44537  infxrbnd2  45820  funressnfv  47513  funressndmafv2rn  47693  iccpartiltu  47904