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  2977  2reu4lem  4476  resopab2  5995  xpco  6247  funconstss  7001  xpopth  7974  xpord2pred  8087  snmapen  8975  ac6sfi  9184  supgtoreq  9374  rankr1bg  9715  alephsdom  9996  brdom7disj  10441  fpwwe2lem12  10553  nn0sub  12451  elznn0  12503  nn01to3  12854  supxrbnd1  13236  supxrbnd2  13237  rexuz3  15272  smueqlem  16417  qnumdenbi  16671  dfiso3  17697  tltnle  18343  lssne0  20902  pjfval2  21664  0top  22927  1stccn  23407  dscopn  24517  bcthlem1  25280  ovolgelb  25437  iblpos  25750  itgposval  25753  itgsubstlem  26011  sincosq3sgn  26465  sincosq4sgn  26466  lgsquadlem3  27349  elzs2  28395  colinearalg  28983  elntg2  29058  wlklnwwlkln2lem  29955  2pthdlem1  30003  wwlks2onsym  30033  rusgrnumwwlkb0  30047  numclwwlk2lem1  30451  nmoo0  30866  leop3  32200  leoptri  32211  f1od2  32798  fedgmullem2  33787  r1ssel  35263  vonf1owev  35302  dfrdg4  36145  curf  37795  poimirlem28  37845  itgaddnclem2  37876  relssinxpdmrn  38538  lfl1dim  39377  glbconxN  39634  2dim  39726  elpadd0  40065  dalawlem13  40139  diclspsn  41450  dihglb2  41598  dochsordN  41630  redvmptabs  42611  lzunuz  43006  tfsconcat0b  43584  uneqsn  44262  ntrclskb  44306  ntrneiel2  44323  infxrbnd2  45609  funressnfv  47285  funressndmafv2rn  47465  iccpartiltu  47664