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  2986  2reu4lem  4522  resopab2  6054  xpco  6309  funconstss  7076  xpopth  8055  xpord2pred  8170  snmapen  9078  ac6sfi  9320  supgtoreq  9510  rankr1bg  9843  alephsdom  10126  brdom7disj  10571  fpwwe2lem12  10682  nn0sub  12576  elznn0  12628  nn01to3  12983  supxrbnd1  13363  supxrbnd2  13364  rexuz3  15387  smueqlem  16527  qnumdenbi  16781  dfiso3  17817  tltnle  18467  lssne0  20949  pjfval2  21729  0top  22990  1stccn  23471  dscopn  24586  bcthlem1  25358  ovolgelb  25515  iblpos  25828  itgposval  25831  itgsubstlem  26089  sincosq3sgn  26542  sincosq4sgn  26543  lgsquadlem3  27426  elzs2  28385  colinearalg  28925  elntg2  29000  wlklnwwlkln2lem  29902  2pthdlem1  29950  wwlks2onsym  29978  rusgrnumwwlkb0  29991  numclwwlk2lem1  30395  nmoo0  30810  leop3  32144  leoptri  32155  f1od2  32732  fedgmullem2  33681  dfrdg4  35952  curf  37605  poimirlem28  37655  itgaddnclem2  37686  relssinxpdmrn  38350  lfl1dim  39122  glbconxN  39380  2dim  39472  elpadd0  39811  dalawlem13  39885  diclspsn  41196  dihglb2  41344  dochsordN  41376  redvmptabs  42390  lzunuz  42779  tfsconcat0b  43359  uneqsn  44038  ntrclskb  44082  ntrneiel2  44099  infxrbnd2  45380  funressnfv  47055  funressndmafv2rn  47235  iccpartiltu  47409