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 206

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 207

This theorem is referenced by:  sbcne12  4395  fnprb  7205  fntpb  7206  eqfunresadj  7358  eloprabga  7521  ordsucuniel  7823  ordsucun  7824  oeoa  8614  ereldm  8774  boxcutc  8960  mapen  9160  mapfien  9425  wemapwe  9716  sdom2en01  10321  prlem936  11066  subcan  11543  mulcan1g  11895  conjmul  11963  ltrec  12129  rebtwnz  12968  xposdif  13283  divelunit  13516  fseq1m1p1  13621  fzm1  13629  fllt  13828  hashfacen  14477  hashf1  14480  ccat0  14599  lenegsq  15344  dvdsmod  16353  bitsmod  16460  smueqlem  16514  rpexp  16746  eulerthlem2  16806  odzdvds  16820  pcelnn  16895  xpsle  17598  isepi  17758  fthmon  17947  cat1  18115  pospropd  18342  grpidpropd  18645  mgmhmpropd  18681  sgrppropd  18714  mndpropd  18742  mhmpropd  18775  grppropd  18939  ghmnsgima  19228  mndodcong  19528  odf1  19548  odf1o1  19558  sylow3lem6  19618  lsmcntzr  19666  efgredlema  19726  cmnpropd  19777  qusecsub  19821  dprdf11  20011  rngpropd  20139  ringpropd  20253  dvdsrpropd  20381  resrhm2b  20567  abvpropd  20800  lmodprop2d  20886  lsspropd  20980  lmhmpropd  21036  lbspropd  21062  lvecvscan  21077  lvecvscan2  21078  chrnzr  21496  zndvds0  21516  ip2eq  21618  phlpropd  21620  assapropd  21837  qtopcn  23657  tsmsf1o  24088  xmetgt0  24302  txmetcnp  24491  metustsym  24499  nlmmul0or  24627  cnmet  24715  evth  24914  isclmp  25053  minveclem3b  25385  mbfposr  25610  itg2cn  25721  iblcnlem  25747  dvcvx  25982  ulm2  26351  efeq1  26494  dcubic  26813  mcubic  26814  dquart  26820  birthdaylem3  26920  ftalem2  27041  issqf  27103  sqff1o  27149  bposlem7  27258  lgsabs1  27304  gausslemma2dlem1a  27333  lgsquadlem2  27349  addsq2reu  27408  dchrisum0lem1  27484  sltrec  27789  opphllem6  28736  colhp  28754  lmiinv  28776  lmiopp  28786  wlkeq  29619  eupth2lem3lem3  30216  eupth2lem3lem6  30219  nmounbi  30762  ip2eqi  30842  hvmulcan  31058  hvsubcan2  31061  hi2eq  31091  fh2  31605  riesz4i  32049  cvbr4i  32353  sgnmulsgn  32826  sgnmulsgp  32827  xdivpnfrp  32912  isorng  33326  qusker  33369  ellspds  33388  ply1moneq  33604  ballotlemfc0  34530  ballotlemfcc  34531  subfacp1lem5  35211  topfneec2  36379  neibastop3  36385  unccur  37632  cos2h  37640  tan2h  37641  poimirlem25  37674  poimirlem27  37676  dvasin  37733  caures  37789  ismtyima  37832  isdmn3  38103  dmecd  38327  releldmqscoss  38683  tendospcanN  41047  dochsncom  41406  f1o2d2  42251  sqrtcval  43640  or3or  44022  neicvgel1  44118  rusbcALT  44438  sbcoreleleqVD  44858  climreeq  45622  coseq0  45873  affinecomb1  48662  eenglngeehlnmlem1  48697  2sphere  48709  line2  48712  itscnhlc0yqe  48719  itscnhlc0xyqsol  48725  oduoppcciso  49423