Theorem bitr2di 291

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bitr4id  293  bibif  375  oranabs  999  necon4bid  2979  2reu4lem  4412  resopab2  5878  xpco  6121  funconstss  6833  xpopth  7755  snmapen  8637  ac6sfi  8836  supgtoreq  9007  rankr1bg  9305  alephsdom  9586  brdom7disj  10031  fpwwe2lem12  10142  nn0sub  12026  elznn0  12077  nn01to3  12423  supxrbnd1  12797  supxrbnd2  12798  rexuz3  14798  smueqlem  15933  qnumdenbi  16184  dfiso3  17148  lssne0  19841  pjfval2  20525  0top  21734  1stccn  22214  dscopn  23326  bcthlem1  24076  ovolgelb  24232  iblpos  24545  itgposval  24548  itgsubstlem  24800  sincosq3sgn  25245  sincosq4sgn  25246  lgsquadlem3  26118  colinearalg  26856  elntg2  26931  wlklnwwlkln2lem  27820  2pthdlem1  27868  wwlks2onsym  27896  rusgrnumwwlkb0  27909  numclwwlk2lem1  28313  nmoo0  28726  leop3  30060  leoptri  30071  f1od2  30631  tltnle  30822  fedgmullem2  31283  xpord2pred  33403  dfrdg4  33891  curf  35378  poimirlem28  35428  itgaddnclem2  35459  lfl1dim  36758  glbconxN  37015  2dim  37107  elpadd0  37446  dalawlem13  37520  diclspsn  38831  dihglb2  38979  dochsordN  39011  lzunuz  40162  uneqsn  41179  ntrclskb  41225  ntrneiel2  41242  infxrbnd2  42446  funressnfv  44076  funressndmafv2rn  44248  iccpartiltu  44408