Theorem bitr2di 287

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 286	. 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  289  bibif  370  oranabs  996  necon4bid  2984  2reu4lem  4524  resopab2  6035  xpco  6287  funconstss  7056  xpopth  8018  xpord2pred  8133  snmapen  9040  ac6sfi  9289  supgtoreq  9467  rankr1bg  9800  alephsdom  10083  brdom7disj  10528  fpwwe2lem12  10639  nn0sub  12526  elznn0  12577  nn01to3  12929  supxrbnd1  13304  supxrbnd2  13305  rexuz3  15299  smueqlem  16435  qnumdenbi  16684  dfiso3  17724  tltnle  18379  lssne0  20705  pjfval2  21483  0top  22706  1stccn  23187  dscopn  24302  bcthlem1  25072  ovolgelb  25229  iblpos  25542  itgposval  25545  itgsubstlem  25800  sincosq3sgn  26246  sincosq4sgn  26247  lgsquadlem3  27121  colinearalg  28435  elntg2  28510  wlklnwwlkln2lem  29403  2pthdlem1  29451  wwlks2onsym  29479  rusgrnumwwlkb0  29492  numclwwlk2lem1  29896  nmoo0  30311  leop3  31645  leoptri  31656  f1od2  32213  fedgmullem2  33003  dfrdg4  35227  curf  36769  poimirlem28  36819  itgaddnclem2  36850  relssinxpdmrn  37521  lfl1dim  38294  glbconxN  38552  2dim  38644  elpadd0  38983  dalawlem13  39057  diclspsn  40368  dihglb2  40516  dochsordN  40548  lzunuz  41808  tfsconcat0b  42398  uneqsn  43078  ntrclskb  43122  ntrneiel2  43139  infxrbnd2  44377  funressnfv  46051  funressndmafv2rn  46229  iccpartiltu  46388