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  2973  2reu4lem  4472  resopab2  5985  xpco  6236  funconstss  6989  xpopth  7962  xpord2pred  8075  snmapen  8960  ac6sfi  9168  supgtoreq  9355  rankr1bg  9693  alephsdom  9974  brdom7disj  10419  fpwwe2lem12  10530  nn0sub  12428  elznn0  12480  nn01to3  12836  supxrbnd1  13217  supxrbnd2  13218  rexuz3  15253  smueqlem  16398  qnumdenbi  16652  dfiso3  17677  tltnle  18323  lssne0  20882  pjfval2  21644  0top  22896  1stccn  23376  dscopn  24486  bcthlem1  25249  ovolgelb  25406  iblpos  25719  itgposval  25722  itgsubstlem  25980  sincosq3sgn  26434  sincosq4sgn  26435  lgsquadlem3  27318  elzs2  28321  colinearalg  28886  elntg2  28961  wlklnwwlkln2lem  29858  2pthdlem1  29906  wwlks2onsym  29934  rusgrnumwwlkb0  29947  numclwwlk2lem1  30351  nmoo0  30766  leop3  32100  leoptri  32111  f1od2  32697  fedgmullem2  33638  r1ssel  35109  vonf1owev  35140  dfrdg4  35984  curf  37637  poimirlem28  37687  itgaddnclem2  37718  relssinxpdmrn  38376  lfl1dim  39159  glbconxN  39416  2dim  39508  elpadd0  39847  dalawlem13  39921  diclspsn  41232  dihglb2  41380  dochsordN  41412  redvmptabs  42392  lzunuz  42800  tfsconcat0b  43378  uneqsn  44057  ntrclskb  44101  ntrneiel2  44118  infxrbnd2  45406  funressnfv  47073  funressndmafv2rn  47253  iccpartiltu  47452