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  1002  necon4bid  2978  2reu4lem  4478  resopab2  6003  xpco  6255  funconstss  7010  xpopth  7984  xpord2pred  8097  snmapen  8987  ac6sfi  9196  supgtoreq  9386  rankr1bg  9727  alephsdom  10008  brdom7disj  10453  fpwwe2lem12  10565  nn0sub  12463  elznn0  12515  nn01to3  12866  supxrbnd1  13248  supxrbnd2  13249  rexuz3  15284  smueqlem  16429  qnumdenbi  16683  dfiso3  17709  tltnle  18355  lssne0  20914  pjfval2  21676  0top  22939  1stccn  23419  dscopn  24529  bcthlem1  25292  ovolgelb  25449  iblpos  25762  itgposval  25765  itgsubstlem  26023  sincosq3sgn  26477  sincosq4sgn  26478  lgsquadlem3  27361  elzs2  28407  colinearalg  28995  elntg2  29070  wlklnwwlkln2lem  29967  2pthdlem1  30015  wwlks2onsym  30045  rusgrnumwwlkb0  30059  numclwwlk2lem1  30463  nmoo0  30878  leop3  32212  leoptri  32223  f1od2  32808  fedgmullem2  33807  r1ssel  35282  vonf1owev  35321  dfrdg4  36164  curf  37843  poimirlem28  37893  itgaddnclem2  37924  relssinxpdmrn  38594  lfl1dim  39491  glbconxN  39748  2dim  39840  elpadd0  40179  dalawlem13  40253  diclspsn  41564  dihglb2  41712  dochsordN  41744  redvmptabs  42724  lzunuz  43119  tfsconcat0b  43697  uneqsn  44375  ntrclskb  44419  ntrneiel2  44436  infxrbnd2  45721  funressnfv  47397  funressndmafv2rn  47577  iccpartiltu  47776