Theorem 3bitr3d 297

Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.)

Hypotheses

Ref	Expression
3bitr3d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr3d.2	⊢ (𝜑 → (𝜓 ↔ 𝜃))
3bitr3d.3	⊢ (𝜑 → (𝜒 ↔ 𝜏))

Assertion

Ref	Expression
3bitr3d	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Proof of Theorem 3bitr3d

Step	Hyp	Ref	Expression
1		3bitr3d.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
2		3bitr3d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	bitr3d 269	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3d.3	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜏))
5	3, 4	bitrd 267	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  sbcne12  3938  fnprb  6377  fntpb  6378  eloprabga  6645  ordsucuniel  6916  ordsucun  6917  oeoa  7564  ereldm  7677  boxcutc  7837  mapen  8009  mapfien  8196  wemapwe  8477  sdom2en01  9007  prlem936  9748  subcan  10215  mulcan1g  10559  conjmul  10621  ltrec  10784  rebtwnz  11663  xposdif  11964  divelunit  12185  fseq1m1p1  12284  fzm1  12289  fllt  12469  hashfacen  13095  hashf1  13098  lenegsq  13908  dvdsmod  14888  bitsmod  14996  smueqlem  15050  rpexp  15270  eulerthlem2  15325  odzdvds  15338  pcelnn  15412  xpsle  16064  isepi  16223  fthmon  16410  pospropd  16957  grpidpropd  17084  mndpropd  17139  mhmpropd  17164  grppropd  17260  ghmnsgima  17507  mndodcong  17784  odf1  17802  odf1o1  17810  sylow3lem6  17870  lsmcntzr  17916  efgredlema  17976  cmnpropd  18025  dprdf11  18245  ringpropd  18405  dvdsrpropd  18519  abvpropd  18665  lmodprop2d  18748  lsspropd  18838  lmhmpropd  18894  lbspropd  18920  lvecvscan  18932  lvecvscan2  18933  assapropd  19148  chrnzr  19697  zndvds0  19718  ip2eq  19817  phlpropd  19819  qtopcn  21327  tsmsf1o  21758  xmetgt0  21973  txmetcnp  22162  metustsym  22170  nlmmul0or  22297  cnmet  22385  evth  22566  isclmp  22705  minveclem3b  23007  mbfposr  23225  itg2cn  23336  iblcnlem  23361  dvcvx  23587  ulm2  23943  efeq1  24079  dcubic  24373  mcubic  24374  dquart  24380  birthdaylem3  24480  ftalem2  24600  issqf  24662  sqff1o  24708  bposlem7  24815  lgsabs1  24861  gausslemma2dlem1a  24890  lgsquadlem2  24906  dchrisum0lem1  25005  opphllem6  25444  colhp  25462  lmiinv  25484  lmiopp  25494  cusgra2v  25991  eupath2lem3  26506  nmounbi  27015  ip2eqi  27096  hvmulcan  27313  hvsubcan2  27316  hi2eq  27346  fh2  27862  riesz4i  28306  cvbr4i  28610  xdivpnfrp  28972  isorng  29130  ballotlemfc0  29881  ballotlemfcc  29882  sgnmulsgn  29938  sgnmulsgp  29939  subfacp1lem5  30420  topfneec2  31521  neibastop3  31527  unccur  32562  cos2h  32570  tan2h  32571  poimirlem25  32604  poimirlem27  32606  dvasin  32666  caures  32726  ismtyima  32772  isdmn3  33043  tendospcanN  35330  dochsncom  35689  or3or  37339  neicvgel1  37437  rusbcALT  37662  sbc3orgOLD  37763  climreeq  38680  coseq0  38747  eupth2lem3lem3  41398  eupth2lem3lem6  41401  mgmhmpropd  41575