Theorem bitr2di 290

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bitr4id  292  bibif  373  oranabs  1012  necon4bid  3001  2reu4lem  4476  resopab2  6022  xpco  6272  funconstss  7033  xpopth  8007  xpord2pred  8120  snmapen  9015  ac6sfi  9224  supgtoreq  9414  rankr1bg  9758  alephsdom  10039  brdom7disj  10485  fpwwe2lem12  10597  nn0sub  12528  elznn0  12580  nn01to3  12939  supxrbnd1  13321  supxrbnd2  13322  rexuz3  15359  smueqlem  16507  qnumdenbi  16762  dfiso3  17789  tltnle  18435  lssne0  20998  pjfval2  21741  0top  23023  1stccn  23503  dscopn  24613  bcthlem1  25366  ovolgelb  25522  iblpos  25835  itgposval  25838  itgsubstlem  26090  sincosq3sgn  26542  sincosq4sgn  26543  lgsquadlem3  27423  elzs2  28469  colinearalg  29057  elntg2  29132  wlklnwwlkln2lem  30028  2pthdlem1  30076  wwlks2onsym  30106  rusgrnumwwlkb0  30120  numclwwlk2lem1  30524  nmoo0  30940  leop3  32274  leoptri  32285  f1od2  32871  fedgmullem2  33888  r1ssel  35367  vonf1wev  35415  vonf1owevOLD  35417  dfrdg4  36265  mh-regprimbi  36869  curf  38061  poimirlem28  38111  itgaddnclem2  38142  relssinxpdmrn  38812  lfl1dim  39709  glbconxN  39966  2dim  40058  elpadd0  40397  dalawlem13  40471  diclspsn  41782  dihglb2  41930  dochsordN  41962  redvmptabs  42933  lzunuz  43313  tfsconcat0b  43887  uneqsn  44565  ntrclskb  44609  ntrneiel2  44626  infxrbnd2  45908  funressnfv  47601  funressndmafv2rn  47781  iccpartiltu  47992