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  372  oranabs  997  necon4bid  2989  2reu4lem  4456  resopab2  5944  xpco  6192  funconstss  6933  xpopth  7872  snmapen  8828  ac6sfi  9058  supgtoreq  9229  rankr1bg  9561  alephsdom  9842  brdom7disj  10287  fpwwe2lem12  10398  nn0sub  12283  elznn0  12334  nn01to3  12681  supxrbnd1  13055  supxrbnd2  13056  rexuz3  15060  smueqlem  16197  qnumdenbi  16448  dfiso3  17485  tltnle  18140  lssne0  20212  pjfval2  20916  0top  22133  1stccn  22614  dscopn  23729  bcthlem1  24488  ovolgelb  24644  iblpos  24957  itgposval  24960  itgsubstlem  25212  sincosq3sgn  25657  sincosq4sgn  25658  lgsquadlem3  26530  colinearalg  27278  elntg2  27353  wlklnwwlkln2lem  28247  2pthdlem1  28295  wwlks2onsym  28323  rusgrnumwwlkb0  28336  numclwwlk2lem1  28740  nmoo0  29153  leop3  30487  leoptri  30498  f1od2  31056  fedgmullem2  31711  xpord2pred  33792  dfrdg4  34253  curf  35755  poimirlem28  35805  itgaddnclem2  35836  lfl1dim  37135  glbconxN  37392  2dim  37484  elpadd0  37823  dalawlem13  37897  diclspsn  39208  dihglb2  39356  dochsordN  39388  lzunuz  40590  uneqsn  41633  ntrclskb  41679  ntrneiel2  41696  infxrbnd2  42908  funressnfv  44537  funressndmafv2rn  44715  iccpartiltu  44874