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  3000  2reu4lem  4478  resopab2  6027  xpco  6292  funconstss  7056  xpopth  8043  f1od2  8111  xpord2pred  8165  curf  8894  snmapen  9070  ac6sfi  9279  supgtoreq  9467  rankr1bg  9815  alephsdom  10169  brdom7disj  10614  fpwwe2lem12  10731  nn0sub  12660  elznn0  12712  nn01to3  13072  supxrbnd1  13455  supxrbnd2  13456  rexuz3  15522  smueqlem  16666  qnumdenbi  16926  dfiso3  17954  tltnle  18600  lssne0  21232  pjfval2  22021  0top  23307  1stccn  23788  dscopn  24898  bcthlem1  25651  ovolgelb  25807  iblpos  26119  itgposval  26122  itgsubstlem  26374  sincosq3sgn  26835  sincosq4sgn  26836  lgsquadlem3  27715  elzs2  28791  colinearalg  29494  elntg2  29569  wlklnwwlkln2lem  30477  2pthdlem1  30525  wwlks2onsym  30555  rusgrnumwwlkb0  30569  numclwwlk2lem1  30983  nmoo0  31399  leop3  32733  leoptri  32744  fedgmullem2  34309  r1ssel  35785  vonf1wev  35956  vonf1owevOLD  35958  dfrdg4  36808  mh-regprimbi  37426  poimirlem28  38660  itgaddnclem2  38691  relssinxpdmrn  39375  lfl1dim  40272  glbconxN  40529  2dim  40621  elpadd0  40960  dalawlem13  41034  diclspsn  42345  dihglb2  42493  dochsordN  42525  redvmptabs  43505  lzunuz  43873  tfsconcat0b  44442  uneqsn  45119  ntrclskb  45163  ntrneiel2  45180  infxrbnd2  46474  funressnfv  48207  funressndmafv2rn  48387  iccpartiltu  48598