Theorem 3bitr3d 309

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 281	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3d.3	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜏))
5	3, 4	bitrd 279	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:  sbcne12  4411  fnprb  7205  fntpb  7206  eqfunresadj  7352  eloprabga  7511  eloprabgaOLD  7512  ordsucuniel  7807  ordsucun  7808  oeoa  8593  ereldm  8747  boxcutc  8931  mapen  9137  mapfien  9399  wemapwe  9688  sdom2en01  10293  prlem936  11038  subcan  11511  mulcan1g  11863  conjmul  11927  ltrec  12092  rebtwnz  12927  xposdif  13237  divelunit  13467  fseq1m1p1  13572  fzm1  13577  fllt  13767  hashfacen  14409  hashfacenOLD  14410  hashf1  14414  ccat0  14522  lenegsq  15263  dvdsmod  16268  bitsmod  16373  smueqlem  16427  rpexp  16655  eulerthlem2  16711  odzdvds  16724  pcelnn  16799  xpsle  17521  isepi  17683  fthmon  17874  cat1  18043  pospropd  18276  grpidpropd  18577  sgrppropd  18618  mndpropd  18646  mhmpropd  18674  grppropd  18833  ghmnsgima  19110  mndodcong  19403  odf1  19423  odf1o1  19433  sylow3lem6  19493  lsmcntzr  19541  efgredlema  19601  cmnpropd  19652  qusecsub  19695  dprdf11  19885  ringpropd  20092  dvdsrpropd  20219  resrhm2b  20382  abvpropd  20438  lmodprop2d  20522  lsspropd  20616  lmhmpropd  20672  lbspropd  20698  lvecvscan  20712  lvecvscan2  20713  chrnzr  21066  zndvds0  21090  ip2eq  21190  phlpropd  21192  assapropd  21408  qtopcn  23200  tsmsf1o  23631  xmetgt0  23846  txmetcnp  24038  metustsym  24046  nlmmul0or  24182  cnmet  24270  evth  24457  isclmp  24595  minveclem3b  24927  mbfposr  25151  itg2cn  25263  iblcnlem  25288  dvcvx  25519  ulm2  25879  efeq1  26019  dcubic  26331  mcubic  26332  dquart  26338  birthdaylem3  26438  ftalem2  26558  issqf  26620  sqff1o  26666  bposlem7  26773  lgsabs1  26819  gausslemma2dlem1a  26848  lgsquadlem2  26864  addsq2reu  26923  dchrisum0lem1  26999  sltrec  27301  opphllem6  27983  colhp  28001  lmiinv  28023  lmiopp  28033  wlkeq  28871  eupth2lem3lem3  29463  eupth2lem3lem6  29466  nmounbi  30007  ip2eqi  30087  hvmulcan  30303  hvsubcan2  30306  hi2eq  30336  fh2  30850  riesz4i  31294  cvbr4i  31598  xdivpnfrp  32077  isorng  32386  qusker  32433  ellspds  32450  ply1moneq  32612  ballotlemfc0  33429  ballotlemfcc  33430  sgnmulsgn  33486  sgnmulsgp  33487  subfacp1lem5  34113  topfneec2  35179  neibastop3  35185  unccur  36409  cos2h  36417  tan2h  36418  poimirlem25  36451  poimirlem27  36453  dvasin  36510  caures  36566  ismtyima  36609  isdmn3  36880  dmecd  37111  releldmqscoss  37468  tendospcanN  39832  dochsncom  40191  f1o2d2  41004  sqrtcval  42325  or3or  42707  neicvgel1  42803  rusbcALT  43131  sbcoreleleqVD  43553  climreeq  44264  coseq0  44515  mgmhmpropd  46490  rngpropd  46608  affinecomb1  47290  eenglngeehlnmlem1  47325  2sphere  47337  line2  47340  itscnhlc0yqe  47347  itscnhlc0xyqsol  47353