Theorem bitr2di 287

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 286	. 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  289  bibif  371  oranabs  996  necon4bid  2988  2reu4lem  4453  resopab2  5933  xpco  6181  funconstss  6915  xpopth  7845  snmapen  8782  ac6sfi  8988  supgtoreq  9159  rankr1bg  9492  alephsdom  9773  brdom7disj  10218  fpwwe2lem12  10329  nn0sub  12213  elznn0  12264  nn01to3  12610  supxrbnd1  12984  supxrbnd2  12985  rexuz3  14988  smueqlem  16125  qnumdenbi  16376  dfiso3  17402  tltnle  18055  lssne0  20127  pjfval2  20826  0top  22041  1stccn  22522  dscopn  23635  bcthlem1  24393  ovolgelb  24549  iblpos  24862  itgposval  24865  itgsubstlem  25117  sincosq3sgn  25562  sincosq4sgn  25563  lgsquadlem3  26435  colinearalg  27181  elntg2  27256  wlklnwwlkln2lem  28148  2pthdlem1  28196  wwlks2onsym  28224  rusgrnumwwlkb0  28237  numclwwlk2lem1  28641  nmoo0  29054  leop3  30388  leoptri  30399  f1od2  30958  fedgmullem2  31613  xpord2pred  33719  dfrdg4  34180  curf  35682  poimirlem28  35732  itgaddnclem2  35763  lfl1dim  37062  glbconxN  37319  2dim  37411  elpadd0  37750  dalawlem13  37824  diclspsn  39135  dihglb2  39283  dochsordN  39315  lzunuz  40506  uneqsn  41522  ntrclskb  41568  ntrneiel2  41585  infxrbnd2  42798  funressnfv  44424  funressndmafv2rn  44602  iccpartiltu  44762