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  4413  fnprb  7210  fntpb  7211  eqfunresadj  7357  eloprabga  7516  eloprabgaOLD  7517  ordsucuniel  7812  ordsucun  7813  oeoa  8597  ereldm  8751  boxcutc  8935  mapen  9141  mapfien  9403  wemapwe  9692  sdom2en01  10297  prlem936  11042  subcan  11515  mulcan1g  11867  conjmul  11931  ltrec  12096  rebtwnz  12931  xposdif  13241  divelunit  13471  fseq1m1p1  13576  fzm1  13581  fllt  13771  hashfacen  14413  hashfacenOLD  14414  hashf1  14418  ccat0  14526  lenegsq  15267  dvdsmod  16272  bitsmod  16377  smueqlem  16431  rpexp  16659  eulerthlem2  16715  odzdvds  16728  pcelnn  16803  xpsle  17525  isepi  17687  fthmon  17878  cat1  18047  pospropd  18280  grpidpropd  18581  sgrppropd  18622  mndpropd  18650  mhmpropd  18678  grppropd  18837  ghmnsgima  19116  mndodcong  19410  odf1  19430  odf1o1  19440  sylow3lem6  19500  lsmcntzr  19548  efgredlema  19608  cmnpropd  19659  qusecsub  19703  dprdf11  19893  ringpropd  20102  dvdsrpropd  20230  resrhm2b  20349  abvpropd  20450  lmodprop2d  20534  lsspropd  20628  lmhmpropd  20684  lbspropd  20710  lvecvscan  20724  lvecvscan2  20725  chrnzr  21082  zndvds0  21106  ip2eq  21206  phlpropd  21208  assapropd  21426  qtopcn  23218  tsmsf1o  23649  xmetgt0  23864  txmetcnp  24056  metustsym  24064  nlmmul0or  24200  cnmet  24288  evth  24475  isclmp  24613  minveclem3b  24945  mbfposr  25169  itg2cn  25281  iblcnlem  25306  dvcvx  25537  ulm2  25897  efeq1  26037  dcubic  26351  mcubic  26352  dquart  26358  birthdaylem3  26458  ftalem2  26578  issqf  26640  sqff1o  26686  bposlem7  26793  lgsabs1  26839  gausslemma2dlem1a  26868  lgsquadlem2  26884  addsq2reu  26943  dchrisum0lem1  27019  sltrec  27321  opphllem6  28003  colhp  28021  lmiinv  28043  lmiopp  28053  wlkeq  28891  eupth2lem3lem3  29483  eupth2lem3lem6  29486  nmounbi  30029  ip2eqi  30109  hvmulcan  30325  hvsubcan2  30328  hi2eq  30358  fh2  30872  riesz4i  31316  cvbr4i  31620  xdivpnfrp  32099  isorng  32417  qusker  32464  ellspds  32481  ply1moneq  32665  ballotlemfc0  33491  ballotlemfcc  33492  sgnmulsgn  33548  sgnmulsgp  33549  subfacp1lem5  34175  topfneec2  35241  neibastop3  35247  unccur  36471  cos2h  36479  tan2h  36480  poimirlem25  36513  poimirlem27  36515  dvasin  36572  caures  36628  ismtyima  36671  isdmn3  36942  dmecd  37173  releldmqscoss  37530  tendospcanN  39894  dochsncom  40253  f1o2d2  41055  sqrtcval  42392  or3or  42774  neicvgel1  42870  rusbcALT  43198  sbcoreleleqVD  43620  climreeq  44329  coseq0  44580  mgmhmpropd  46555  rngpropd  46673  affinecomb1  47388  eenglngeehlnmlem1  47423  2sphere  47435  line2  47438  itscnhlc0yqe  47445  itscnhlc0xyqsol  47451