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  3001  2reu4lem  4479  resopab2  6030  xpco  6285  funconstss  7047  xpopth  8031  xpord2pred  8146  curf  8874  snmapen  9050  ac6sfi  9259  supgtoreq  9447  rankr1bg  9793  alephsdom  10146  brdom7disj  10591  fpwwe2lem12  10708  nn0sub  12637  elznn0  12689  nn01to3  13049  supxrbnd1  13432  supxrbnd2  13433  rexuz3  15496  smueqlem  16640  qnumdenbi  16900  dfiso3  17928  tltnle  18574  lssne0  21206  pjfval2  21995  0top  23281  1stccn  23762  dscopn  24872  bcthlem1  25625  ovolgelb  25781  iblpos  26093  itgposval  26096  itgsubstlem  26348  sincosq3sgn  26811  sincosq4sgn  26812  lgsquadlem3  27691  elzs2  28767  colinearalg  29470  elntg2  29545  wlklnwwlkln2lem  30453  2pthdlem1  30501  wwlks2onsym  30531  rusgrnumwwlkb0  30545  numclwwlk2lem1  30959  nmoo0  31375  leop3  32709  leoptri  32720  f1od2  33293  fedgmullem2  34244  r1ssel  35711  vonf1wev  35860  vonf1owevOLD  35862  dfrdg4  36685  mh-regprimbi  37303  poimirlem28  38534  itgaddnclem2  38565  relssinxpdmrn  39249  lfl1dim  40146  glbconxN  40403  2dim  40495  elpadd0  40834  dalawlem13  40908  diclspsn  42219  dihglb2  42367  dochsordN  42399  redvmptabs  43379  lzunuz  43732  tfsconcat0b  44306  uneqsn  44984  ntrclskb  45028  ntrneiel2  45045  infxrbnd2  46324  funressnfv  48057  funressndmafv2rn  48237  iccpartiltu  48448