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  2978  2reu4lem  4478  resopab2  6005  xpco  6257  funconstss  7012  xpopth  7986  xpord2pred  8099  snmapen  8989  ac6sfi  9198  supgtoreq  9388  rankr1bg  9729  alephsdom  10010  brdom7disj  10455  fpwwe2lem12  10567  nn0sub  12465  elznn0  12517  nn01to3  12868  supxrbnd1  13250  supxrbnd2  13251  rexuz3  15286  smueqlem  16431  qnumdenbi  16685  dfiso3  17711  tltnle  18357  lssne0  20919  pjfval2  21681  0top  22944  1stccn  23424  dscopn  24534  bcthlem1  25297  ovolgelb  25454  iblpos  25767  itgposval  25770  itgsubstlem  26028  sincosq3sgn  26482  sincosq4sgn  26483  lgsquadlem3  27366  elzs2  28412  colinearalg  29001  elntg2  29076  wlklnwwlkln2lem  29973  2pthdlem1  30021  wwlks2onsym  30051  rusgrnumwwlkb0  30065  numclwwlk2lem1  30469  nmoo0  30885  leop3  32219  leoptri  32230  f1od2  32815  fedgmullem2  33814  r1ssel  35290  vonf1owev  35330  dfrdg4  36173  curf  37878  poimirlem28  37928  itgaddnclem2  37959  relssinxpdmrn  38629  lfl1dim  39526  glbconxN  39783  2dim  39875  elpadd0  40214  dalawlem13  40288  diclspsn  41599  dihglb2  41747  dochsordN  41779  redvmptabs  42759  lzunuz  43154  tfsconcat0b  43732  uneqsn  44410  ntrclskb  44454  ntrneiel2  44471  infxrbnd2  45756  funressnfv  47432  funressndmafv2rn  47612  iccpartiltu  47811