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  4497  resopab2  6023  xpco  6278  funconstss  7046  xpopth  8029  xpord2pred  8144  snmapen  9052  ac6sfi  9292  supgtoreq  9483  rankr1bg  9817  alephsdom  10100  brdom7disj  10545  fpwwe2lem12  10656  nn0sub  12551  elznn0  12603  nn01to3  12957  supxrbnd1  13337  supxrbnd2  13338  rexuz3  15367  smueqlem  16509  qnumdenbi  16763  dfiso3  17786  tltnle  18432  lssne0  20908  pjfval2  21669  0top  22921  1stccn  23401  dscopn  24512  bcthlem1  25276  ovolgelb  25433  iblpos  25746  itgposval  25749  itgsubstlem  26007  sincosq3sgn  26461  sincosq4sgn  26462  lgsquadlem3  27345  elzs2  28339  colinearalg  28889  elntg2  28964  wlklnwwlkln2lem  29864  2pthdlem1  29912  wwlks2onsym  29940  rusgrnumwwlkb0  29953  numclwwlk2lem1  30357  nmoo0  30772  leop3  32106  leoptri  32117  f1od2  32698  fedgmullem2  33670  dfrdg4  35969  curf  37622  poimirlem28  37672  itgaddnclem2  37703  relssinxpdmrn  38367  lfl1dim  39139  glbconxN  39397  2dim  39489  elpadd0  39828  dalawlem13  39902  diclspsn  41213  dihglb2  41361  dochsordN  41393  redvmptabs  42403  lzunuz  42791  tfsconcat0b  43370  uneqsn  44049  ntrclskb  44093  ntrneiel2  44110  infxrbnd2  45396  funressnfv  47072  funressndmafv2rn  47252  iccpartiltu  47436