Theorem bitr2di 291

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 290	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4	3	bicomd 226	1 ⊢ (𝜑 → (𝜃 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bitr4id  293  bibif  375  oranabs  997  necon4bid  2996  2reu4lem  4421  resopab2  5880  xpco  6122  funconstss  6821  xpopth  7739  snmapen  8614  ac6sfi  8800  supgtoreq  8972  rankr1bg  9270  alephsdom  9551  brdom7disj  9996  fpwwe2lem12  10107  nn0sub  11989  elznn0  12040  nn01to3  12386  supxrbnd1  12760  supxrbnd2  12761  rexuz3  14761  smueqlem  15894  qnumdenbi  16144  dfiso3  17107  lssne0  19795  pjfval2  20479  0top  21688  1stccn  22168  dscopn  23280  bcthlem1  24029  ovolgelb  24185  iblpos  24497  itgposval  24500  itgsubstlem  24752  sincosq3sgn  25197  sincosq4sgn  25198  lgsquadlem3  26070  colinearalg  26808  elntg2  26883  wlklnwwlkln2lem  27772  2pthdlem1  27820  wwlks2onsym  27848  rusgrnumwwlkb0  27861  numclwwlk2lem1  28265  nmoo0  28678  leop3  30012  leoptri  30023  f1od2  30584  tltnle  30775  fedgmullem2  31236  xpord2pred  33351  dfrdg4  33828  curf  35341  poimirlem28  35391  itgaddnclem2  35422  lfl1dim  36723  glbconxN  36980  2dim  37072  elpadd0  37411  dalawlem13  37485  diclspsn  38796  dihglb2  38944  dochsordN  38976  lzunuz  40110  uneqsn  41127  ntrclskb  41173  ntrneiel2  41190  infxrbnd2  42397  funressnfv  44029  funressndmafv2rn  44175  iccpartiltu  44335