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  2983  2reu4lem  4527  resopab2  6055  xpco  6310  funconstss  7075  xpopth  8053  xpord2pred  8168  snmapen  9076  ac6sfi  9317  supgtoreq  9507  rankr1bg  9840  alephsdom  10123  brdom7disj  10568  fpwwe2lem12  10679  nn0sub  12573  elznn0  12625  nn01to3  12980  supxrbnd1  13359  supxrbnd2  13360  rexuz3  15383  smueqlem  16523  qnumdenbi  16777  dfiso3  17820  tltnle  18479  lssne0  20966  pjfval2  21746  0top  23005  1stccn  23486  dscopn  24601  bcthlem1  25371  ovolgelb  25528  iblpos  25842  itgposval  25845  itgsubstlem  26103  sincosq3sgn  26556  sincosq4sgn  26557  lgsquadlem3  27440  elzs2  28399  colinearalg  28939  elntg2  29014  wlklnwwlkln2lem  29911  2pthdlem1  29959  wwlks2onsym  29987  rusgrnumwwlkb0  30000  numclwwlk2lem1  30404  nmoo0  30819  leop3  32153  leoptri  32164  f1od2  32738  fedgmullem2  33657  dfrdg4  35932  curf  37584  poimirlem28  37634  itgaddnclem2  37665  relssinxpdmrn  38330  lfl1dim  39102  glbconxN  39360  2dim  39452  elpadd0  39791  dalawlem13  39865  diclspsn  41176  dihglb2  41324  dochsordN  41356  redvmptabs  42368  lzunuz  42755  tfsconcat0b  43335  uneqsn  44014  ntrclskb  44058  ntrneiel2  44075  infxrbnd2  45318  funressnfv  46992  funressndmafv2rn  47172  iccpartiltu  47346