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  3004  2reu4lem  4482  resopab2  6041  xpco  6313  funconstss  7081  xpopth  8069  f1od2  8138  xpord2pred  8192  curf  8921  snmapen  9097  ac6sfi  9306  supgtoreq  9493  rankr1bg  9841  alephsdom  10195  brdom7disj  10640  fpwwe2lem12  10757  nn0sub  12686  elznn0  12738  nn01to3  13098  supxrbnd1  13481  supxrbnd2  13482  rexuz3  15548  smueqlem  16692  qnumdenbi  16952  dfiso3  17980  tltnle  18626  lssne0  21259  pjfval2  22048  0top  23334  1stccn  23815  dscopn  24925  bcthlem1  25678  ovolgelb  25834  iblpos  26146  itgposval  26149  itgsubstlem  26401  sincosq3sgn  26862  sincosq4sgn  26863  lgsquadlem3  27742  elzs2  28818  colinearalg  29521  elntg2  29596  wlklnwwlkln2lem  30504  2pthdlem1  30552  wwlks2onsym  30582  rusgrnumwwlkb0  30596  numclwwlk2lem1  31010  nmoo0  31426  leop3  32760  leoptri  32771  fedgmullem2  34345  r1ssel  35827  vonf1wev  36049  vonf1owevOLD  36051  dfrdg4  36906  mh-regprimbi  37524  poimirlem28  38771  itgaddnclem2  38802  relssinxpdmrn  39484  lfl1dim  40381  glbconxN  40638  2dim  40730  elpadd0  41069  dalawlem13  41143  diclspsn  42454  dihglb2  42602  dochsordN  42634  redvmptabs  43615  lzunuz  43983  tfsconcat0b  44551  uneqsn  45228  ntrclskb  45272  ntrneiel2  45289  infxrbnd2  46595  funressnfv  48328  funressndmafv2rn  48508  iccpartiltu  48719