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 222	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bitr4id  290  bibif  371  oranabs  997  necon4bid  2985  2reu4lem  4525  resopab2  6036  xpco  6288  funconstss  7057  xpopth  8020  xpord2pred  8136  snmapen  9044  ac6sfi  9293  supgtoreq  9471  rankr1bg  9804  alephsdom  10087  brdom7disj  10532  fpwwe2lem12  10643  nn0sub  12529  elznn0  12580  nn01to3  12932  supxrbnd1  13307  supxrbnd2  13308  rexuz3  15302  smueqlem  16438  qnumdenbi  16687  dfiso3  17727  tltnle  18385  lssne0  20794  pjfval2  21575  0top  22807  1stccn  23288  dscopn  24403  bcthlem1  25173  ovolgelb  25330  iblpos  25643  itgposval  25646  itgsubstlem  25904  sincosq3sgn  26351  sincosq4sgn  26352  lgsquadlem3  27230  colinearalg  28603  elntg2  28678  wlklnwwlkln2lem  29571  2pthdlem1  29619  wwlks2onsym  29647  rusgrnumwwlkb0  29660  numclwwlk2lem1  30064  nmoo0  30479  leop3  31813  leoptri  31824  f1od2  32381  fedgmullem2  33171  dfrdg4  35395  curf  36933  poimirlem28  36983  itgaddnclem2  37014  relssinxpdmrn  37685  lfl1dim  38458  glbconxN  38716  2dim  38808  elpadd0  39147  dalawlem13  39221  diclspsn  40532  dihglb2  40680  dochsordN  40712  lzunuz  41972  tfsconcat0b  42562  uneqsn  43242  ntrclskb  43286  ntrneiel2  43303  infxrbnd2  44541  funressnfv  46215  funressndmafv2rn  46393  iccpartiltu  46552