Theorem bitr2di 288

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bitr4id  290  bibif  371  oranabs  1001  necon4bid  2970  2reu4lem  4475  resopab2  5991  xpco  6241  funconstss  6994  xpopth  7972  xpord2pred  8085  snmapen  8970  ac6sfi  9189  supgtoreq  9380  rankr1bg  9718  alephsdom  9999  brdom7disj  10444  fpwwe2lem12  10555  nn0sub  12452  elznn0  12504  nn01to3  12860  supxrbnd1  13241  supxrbnd2  13242  rexuz3  15274  smueqlem  16419  qnumdenbi  16673  dfiso3  17698  tltnle  18344  lssne0  20872  pjfval2  21634  0top  22886  1stccn  23366  dscopn  24477  bcthlem1  25240  ovolgelb  25397  iblpos  25710  itgposval  25713  itgsubstlem  25971  sincosq3sgn  26425  sincosq4sgn  26426  lgsquadlem3  27309  elzs2  28310  colinearalg  28873  elntg2  28948  wlklnwwlkln2lem  29845  2pthdlem1  29893  wwlks2onsym  29921  rusgrnumwwlkb0  29934  numclwwlk2lem1  30338  nmoo0  30753  leop3  32087  leoptri  32098  f1od2  32677  fedgmullem2  33602  vonf1owev  35080  dfrdg4  35924  curf  37577  poimirlem28  37627  itgaddnclem2  37658  relssinxpdmrn  38316  lfl1dim  39099  glbconxN  39357  2dim  39449  elpadd0  39788  dalawlem13  39862  diclspsn  41173  dihglb2  41321  dochsordN  41353  redvmptabs  42333  lzunuz  42741  tfsconcat0b  43319  uneqsn  43998  ntrclskb  44042  ntrneiel2  44059  infxrbnd2  45349  funressnfv  47028  funressndmafv2rn  47208  iccpartiltu  47407