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  1001  necon4bid  2970  2reu4lem  4485  resopab2  6007  xpco  6262  funconstss  7028  xpopth  8009  xpord2pred  8124  snmapen  9009  ac6sfi  9231  supgtoreq  9422  rankr1bg  9756  alephsdom  10039  brdom7disj  10484  fpwwe2lem12  10595  nn0sub  12492  elznn0  12544  nn01to3  12900  supxrbnd1  13281  supxrbnd2  13282  rexuz3  15315  smueqlem  16460  qnumdenbi  16714  dfiso3  17735  tltnle  18381  lssne0  20857  pjfval2  21618  0top  22870  1stccn  23350  dscopn  24461  bcthlem1  25224  ovolgelb  25381  iblpos  25694  itgposval  25697  itgsubstlem  25955  sincosq3sgn  26409  sincosq4sgn  26410  lgsquadlem3  27293  elzs2  28287  colinearalg  28837  elntg2  28912  wlklnwwlkln2lem  29812  2pthdlem1  29860  wwlks2onsym  29888  rusgrnumwwlkb0  29901  numclwwlk2lem1  30305  nmoo0  30720  leop3  32054  leoptri  32065  f1od2  32644  fedgmullem2  33626  vonf1owev  35095  dfrdg4  35939  curf  37592  poimirlem28  37642  itgaddnclem2  37673  relssinxpdmrn  38331  lfl1dim  39114  glbconxN  39372  2dim  39464  elpadd0  39803  dalawlem13  39877  diclspsn  41188  dihglb2  41336  dochsordN  41368  redvmptabs  42348  lzunuz  42756  tfsconcat0b  43335  uneqsn  44014  ntrclskb  44058  ntrneiel2  44075  infxrbnd2  45365  funressnfv  47044  funressndmafv2rn  47224  iccpartiltu  47423