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 222	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bitr4id  290  bibif  371  oranabs  997  necon4bid  2985  2reu4lem  4525  resopab2  6036  xpco  6288  funconstss  7057  xpopth  8019  xpord2pred  8134  snmapen  9041  ac6sfi  9290  supgtoreq  9468  rankr1bg  9801  alephsdom  10084  brdom7disj  10529  fpwwe2lem12  10640  nn0sub  12527  elznn0  12578  nn01to3  12930  supxrbnd1  13305  supxrbnd2  13306  rexuz3  15300  smueqlem  16436  qnumdenbi  16685  dfiso3  17725  tltnle  18380  lssne0  20706  pjfval2  21484  0top  22707  1stccn  23188  dscopn  24303  bcthlem1  25073  ovolgelb  25230  iblpos  25543  itgposval  25546  itgsubstlem  25801  sincosq3sgn  26247  sincosq4sgn  26248  lgsquadlem3  27122  colinearalg  28436  elntg2  28511  wlklnwwlkln2lem  29404  2pthdlem1  29452  wwlks2onsym  29480  rusgrnumwwlkb0  29493  numclwwlk2lem1  29897  nmoo0  30312  leop3  31646  leoptri  31657  f1od2  32214  fedgmullem2  33004  dfrdg4  35228  curf  36770  poimirlem28  36820  itgaddnclem2  36851  relssinxpdmrn  37522  lfl1dim  38295  glbconxN  38553  2dim  38645  elpadd0  38984  dalawlem13  39058  diclspsn  40369  dihglb2  40517  dochsordN  40549  lzunuz  41809  tfsconcat0b  42399  uneqsn  43079  ntrclskb  43123  ntrneiel2  43140  infxrbnd2  44378  funressnfv  46052  funressndmafv2rn  46230  iccpartiltu  46389