Theorem bitr2di 291

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 290	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	3	bicomd 226	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bitr4id  293  bibif  374  oranabs  1015  necon4bid  3002  2reu4lem  4482  resopab2  6036  xpco  6291  funconstss  7052  xpopth  8031  xpord2pred  8147  curf  8873  snmapen  9049  ac6sfi  9258  supgtoreq  9445  rankr1bg  9789  alephsdom  10093  brdom7disj  10538  fpwwe2lem12  10655  nn0sub  12582  elznn0  12634  nn01to3  12994  supxrbnd1  13377  supxrbnd2  13378  rexuz3  15440  smueqlem  16586  qnumdenbi  16841  dfiso3  17868  tltnle  18514  lssne0  21141  pjfval2  21928  0top  23214  1stccn  23695  dscopn  24805  bcthlem1  25558  ovolgelb  25714  iblpos  26027  itgposval  26030  itgsubstlem  26282  sincosq3sgn  26745  sincosq4sgn  26746  lgsquadlem3  27626  elzs2  28672  colinearalg  29375  elntg2  29450  wlklnwwlkln2lem  30358  2pthdlem1  30406  wwlks2onsym  30436  rusgrnumwwlkb0  30450  numclwwlk2lem1  30864  nmoo0  31280  leop3  32614  leoptri  32625  f1od2  33198  fedgmullem2  34148  r1ssel  35623  vonf1wev  35713  vonf1owevOLD  35715  dfrdg4  36538  mh-regprimbi  37172  poimirlem28  38405  itgaddnclem2  38436  relssinxpdmrn  39105  lfl1dim  40002  glbconxN  40259  2dim  40351  elpadd0  40690  dalawlem13  40764  diclspsn  42075  dihglb2  42223  dochsordN  42255  redvmptabs  43243  lzunuz  43621  tfsconcat0b  44195  uneqsn  44873  ntrclskb  44917  ntrneiel2  44934  infxrbnd2  46206  funressnfv  47939  funressndmafv2rn  48119  iccpartiltu  48330