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  2974  2reu4lem  4471  resopab2  5989  xpco  6241  funconstss  6995  xpopth  7968  xpord2pred  8081  snmapen  8967  ac6sfi  9175  supgtoreq  9362  rankr1bg  9703  alephsdom  9984  brdom7disj  10429  fpwwe2lem12  10540  nn0sub  12438  elznn0  12490  nn01to3  12841  supxrbnd1  13222  supxrbnd2  13223  rexuz3  15258  smueqlem  16403  qnumdenbi  16657  dfiso3  17682  tltnle  18328  lssne0  20886  pjfval2  21648  0top  22899  1stccn  23379  dscopn  24489  bcthlem1  25252  ovolgelb  25409  iblpos  25722  itgposval  25725  itgsubstlem  25983  sincosq3sgn  26437  sincosq4sgn  26438  lgsquadlem3  27321  elzs2  28324  colinearalg  28890  elntg2  28965  wlklnwwlkln2lem  29862  2pthdlem1  29910  wwlks2onsym  29940  rusgrnumwwlkb0  29954  numclwwlk2lem1  30358  nmoo0  30773  leop3  32107  leoptri  32118  f1od2  32706  fedgmullem2  33664  r1ssel  35139  vonf1owev  35173  dfrdg4  36016  curf  37658  poimirlem28  37708  itgaddnclem2  37739  relssinxpdmrn  38401  lfl1dim  39240  glbconxN  39497  2dim  39589  elpadd0  39928  dalawlem13  40002  diclspsn  41313  dihglb2  41461  dochsordN  41493  redvmptabs  42478  lzunuz  42885  tfsconcat0b  43463  uneqsn  44142  ntrclskb  44186  ntrneiel2  44203  infxrbnd2  45491  funressnfv  47167  funressndmafv2rn  47347  iccpartiltu  47546