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  3006  2reu4lem  4489  resopab2  6043  xpco  6297  funconstss  7058  xpopth  8036  xpord2pred  8150  snmapen  9045  ac6sfi  9254  supgtoreq  9441  rankr1bg  9785  alephsdom  10089  brdom7disj  10533  fpwwe2lem12  10645  nn0sub  12572  elznn0  12624  nn01to3  12983  supxrbnd1  13365  supxrbnd2  13366  rexuz3  15426  smueqlem  16573  qnumdenbi  16828  dfiso3  17855  tltnle  18501  lssne0  21109  pjfval2  21896  0top  23177  1stccn  23657  dscopn  24767  bcthlem1  25520  ovolgelb  25676  iblpos  25989  itgposval  25992  itgsubstlem  26244  sincosq3sgn  26702  sincosq4sgn  26703  lgsquadlem3  27583  elzs2  28629  colinearalg  29297  elntg2  29372  wlklnwwlkln2lem  30268  2pthdlem1  30316  wwlks2onsym  30346  rusgrnumwwlkb0  30360  numclwwlk2lem1  30764  nmoo0  31180  leop3  32514  leoptri  32525  f1od2  33101  fedgmullem2  34051  r1ssel  35526  vonf1wev  35616  vonf1owevOLD  35618  dfrdg4  36464  mh-regprimbi  37097  curf  38290  poimirlem28  38340  itgaddnclem2  38371  relssinxpdmrn  39039  lfl1dim  39936  glbconxN  40193  2dim  40285  elpadd0  40624  dalawlem13  40698  diclspsn  42009  dihglb2  42157  dochsordN  42189  redvmptabs  43162  lzunuz  43540  tfsconcat0b  44114  uneqsn  44792  ntrclskb  44836  ntrneiel2  44853  infxrbnd2  46125  funressnfv  47821  funressndmafv2rn  48001  iccpartiltu  48212