Theorem bitr2di 291

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 290	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	3	bicomd 226	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bitr4id  293  bibif  374  oranabs  1015  necon4bid  3005  2reu4lem  4480  resopab2  6028  xpco  6279  funconstss  7041  xpopth  8015  xpord2pred  8129  snmapen  9023  ac6sfi  9232  supgtoreq  9419  rankr1bg  9763  alephsdom  10058  brdom7disj  10503  fpwwe2lem12  10615  nn0sub  12542  elznn0  12594  nn01to3  12953  supxrbnd1  13335  supxrbnd2  13336  rexuz3  15388  smueqlem  16536  qnumdenbi  16791  dfiso3  17818  tltnle  18464  lssne0  21038  pjfval2  21816  0top  23097  1stccn  23577  dscopn  24687  bcthlem1  25440  ovolgelb  25596  iblpos  25909  itgposval  25912  itgsubstlem  26164  sincosq3sgn  26619  sincosq4sgn  26620  lgsquadlem3  27500  elzs2  28546  colinearalg  29165  elntg2  29240  wlklnwwlkln2lem  30136  2pthdlem1  30184  wwlks2onsym  30214  rusgrnumwwlkb0  30228  numclwwlk2lem1  30632  nmoo0  31048  leop3  32382  leoptri  32393  f1od2  32972  fedgmullem2  33932  r1ssel  35410  vonf1wev  35458  vonf1owevOLD  35460  dfrdg4  36309  mh-regprimbi  36913  curf  38104  poimirlem28  38154  itgaddnclem2  38185  relssinxpdmrn  38855  lfl1dim  39752  glbconxN  40009  2dim  40101  elpadd0  40440  dalawlem13  40514  diclspsn  41825  dihglb2  41973  dochsordN  42005  redvmptabs  42976  lzunuz  43356  tfsconcat0b  43930  uneqsn  44608  ntrclskb  44652  ntrneiel2  44669  infxrbnd2  45943  funressnfv  47636  funressndmafv2rn  47816  iccpartiltu  48027