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 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bitr4id  293  bibif  374  oranabs  1015  necon4bid  3003  2reu4lem  4485  resopab2  6040  xpco  6292  funconstss  7053  xpopth  8028  xpord2pred  8142  snmapen  9036  ac6sfi  9245  supgtoreq  9432  rankr1bg  9776  alephsdom  10071  brdom7disj  10516  fpwwe2lem12  10628  nn0sub  12555  elznn0  12607  nn01to3  12966  supxrbnd1  13348  supxrbnd2  13349  rexuz3  15402  smueqlem  16549  qnumdenbi  16804  dfiso3  17831  tltnle  18477  lssne0  21053  pjfval2  21840  0top  23121  1stccn  23601  dscopn  24711  bcthlem1  25464  ovolgelb  25620  iblpos  25933  itgposval  25936  itgsubstlem  26188  sincosq3sgn  26646  sincosq4sgn  26647  lgsquadlem3  27527  elzs2  28573  colinearalg  29241  elntg2  29316  wlklnwwlkln2lem  30212  2pthdlem1  30260  wwlks2onsym  30290  rusgrnumwwlkb0  30304  numclwwlk2lem1  30708  nmoo0  31124  leop3  32458  leoptri  32469  f1od2  33045  fedgmullem2  34001  r1ssel  35482  vonf1wev  35573  vonf1owevOLD  35575  dfrdg4  36424  mh-regprimbi  37037  curf  38230  poimirlem28  38280  itgaddnclem2  38311  relssinxpdmrn  38979  lfl1dim  39876  glbconxN  40133  2dim  40225  elpadd0  40564  dalawlem13  40638  diclspsn  41949  dihglb2  42097  dochsordN  42129  redvmptabs  43102  lzunuz  43482  tfsconcat0b  44056  uneqsn  44734  ntrclskb  44778  ntrneiel2  44795  infxrbnd2  46067  funressnfv  47763  funressndmafv2rn  47943  iccpartiltu  48154