Theorem bitr2di 288

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 287	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	3	bicomd 223	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bitr4id  290  bibif  371  oranabs  1002  necon4bid  2978  2reu4lem  4464  resopab2  5995  xpco  6247  funconstss  7002  xpopth  7976  xpord2pred  8088  snmapen  8978  ac6sfi  9187  supgtoreq  9377  rankr1bg  9718  alephsdom  9999  brdom7disj  10444  fpwwe2lem12  10556  nn0sub  12478  elznn0  12530  nn01to3  12882  supxrbnd1  13264  supxrbnd2  13265  rexuz3  15302  smueqlem  16450  qnumdenbi  16705  dfiso3  17731  tltnle  18377  lssne0  20937  pjfval2  21699  0top  22958  1stccn  23438  dscopn  24548  bcthlem1  25301  ovolgelb  25457  iblpos  25770  itgposval  25773  itgsubstlem  26025  sincosq3sgn  26477  sincosq4sgn  26478  lgsquadlem3  27359  elzs2  28405  colinearalg  28993  elntg2  29068  wlklnwwlkln2lem  29965  2pthdlem1  30013  wwlks2onsym  30043  rusgrnumwwlkb0  30057  numclwwlk2lem1  30461  nmoo0  30877  leop3  32211  leoptri  32222  f1od2  32807  fedgmullem2  33790  r1ssel  35266  vonf1owev  35306  dfrdg4  36149  mh-regprimbi  36743  curf  37933  poimirlem28  37983  itgaddnclem2  38014  relssinxpdmrn  38684  lfl1dim  39581  glbconxN  39838  2dim  39930  elpadd0  40269  dalawlem13  40343  diclspsn  41654  dihglb2  41802  dochsordN  41834  redvmptabs  42806  lzunuz  43214  tfsconcat0b  43792  uneqsn  44470  ntrclskb  44514  ntrneiel2  44531  infxrbnd2  45816  funressnfv  47503  funressndmafv2rn  47683  iccpartiltu  47894