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  1001  necon4bid  2971  2reu4lem  4488  resopab2  6010  xpco  6265  funconstss  7031  xpopth  8012  xpord2pred  8127  snmapen  9012  ac6sfi  9238  supgtoreq  9429  rankr1bg  9763  alephsdom  10046  brdom7disj  10491  fpwwe2lem12  10602  nn0sub  12499  elznn0  12551  nn01to3  12907  supxrbnd1  13288  supxrbnd2  13289  rexuz3  15322  smueqlem  16467  qnumdenbi  16721  dfiso3  17742  tltnle  18388  lssne0  20864  pjfval2  21625  0top  22877  1stccn  23357  dscopn  24468  bcthlem1  25231  ovolgelb  25388  iblpos  25701  itgposval  25704  itgsubstlem  25962  sincosq3sgn  26416  sincosq4sgn  26417  lgsquadlem3  27300  elzs2  28294  colinearalg  28844  elntg2  28919  wlklnwwlkln2lem  29819  2pthdlem1  29867  wwlks2onsym  29895  rusgrnumwwlkb0  29908  numclwwlk2lem1  30312  nmoo0  30727  leop3  32061  leoptri  32072  f1od2  32651  fedgmullem2  33633  vonf1owev  35102  dfrdg4  35946  curf  37599  poimirlem28  37649  itgaddnclem2  37680  relssinxpdmrn  38338  lfl1dim  39121  glbconxN  39379  2dim  39471  elpadd0  39810  dalawlem13  39884  diclspsn  41195  dihglb2  41343  dochsordN  41375  redvmptabs  42355  lzunuz  42763  tfsconcat0b  43342  uneqsn  44021  ntrclskb  44065  ntrneiel2  44082  infxrbnd2  45372  funressnfv  47048  funressndmafv2rn  47228  iccpartiltu  47427