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  1002  necon4bid  2977  2reu4lem  4463  resopab2  6001  xpco  6253  funconstss  7008  xpopth  7983  xpord2pred  8095  snmapen  8985  ac6sfi  9194  supgtoreq  9384  rankr1bg  9727  alephsdom  10008  brdom7disj  10453  fpwwe2lem12  10565  nn0sub  12487  elznn0  12539  nn01to3  12891  supxrbnd1  13273  supxrbnd2  13274  rexuz3  15311  smueqlem  16459  qnumdenbi  16714  dfiso3  17740  tltnle  18386  lssne0  20946  pjfval2  21689  0top  22948  1stccn  23428  dscopn  24538  bcthlem1  25291  ovolgelb  25447  iblpos  25760  itgposval  25763  itgsubstlem  26015  sincosq3sgn  26464  sincosq4sgn  26465  lgsquadlem3  27345  elzs2  28391  colinearalg  28979  elntg2  29054  wlklnwwlkln2lem  29950  2pthdlem1  29998  wwlks2onsym  30028  rusgrnumwwlkb0  30042  numclwwlk2lem1  30446  nmoo0  30862  leop3  32196  leoptri  32207  f1od2  32792  fedgmullem2  33774  r1ssel  35250  vonf1owev  35290  dfrdg4  36133  mh-regprimbi  36727  curf  37919  poimirlem28  37969  itgaddnclem2  38000  relssinxpdmrn  38670  lfl1dim  39567  glbconxN  39824  2dim  39916  elpadd0  40255  dalawlem13  40329  diclspsn  41640  dihglb2  41788  dochsordN  41820  redvmptabs  42792  lzunuz  43200  tfsconcat0b  43774  uneqsn  44452  ntrclskb  44496  ntrneiel2  44513  infxrbnd2  45798  funressnfv  47491  funressndmafv2rn  47671  iccpartiltu  47882