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  4368  fnprb  7156  fntpb  7157  eqfunresadj  7308  eloprabga  7469  ordsucuniel  7768  ordsucun  7769  oeoa  8527  ereldm  8691  boxcutc  8883  mapen  9073  mapfien  9315  wemapwe  9610  sdom2en01  10216  prlem936  10962  subcan  11440  mulcan1g  11794  conjmul  11862  ltrec  12028  rebtwnz  12864  xposdif  13181  divelunit  13414  fseq1m1p1  13519  fzm1  13527  fllt  13730  hashfacen  14381  hashf1  14384  ccat0  14503  lenegsq  15248  dvdsmod  16260  bitsmod  16367  smueqlem  16421  rpexp  16653  eulerthlem2  16713  odzdvds  16727  pcelnn  16802  xpsle  17504  isepi  17668  fthmon  17857  cat1  18025  pospropd  18252  grpidpropd  18591  mgmhmpropd  18627  sgrppropd  18660  mndpropd  18688  mhmpropd  18721  grppropd  18885  ghmnsgima  19173  mndodcong  19475  odf1  19495  odf1o1  19505  sylow3lem6  19565  lsmcntzr  19613  efgredlema  19673  cmnpropd  19724  qusecsub  19768  dprdf11  19958  rngpropd  20113  ringpropd  20227  dvdsrpropd  20356  resrhm2b  20539  abvpropd  20772  isorng  20798  lmodprop2d  20879  lsspropd  20973  lmhmpropd  21029  lbspropd  21055  lvecvscan  21070  lvecvscan2  21071  chrnzr  21489  zndvds0  21509  ip2eq  21612  phlpropd  21614  assapropd  21831  qtopcn  23662  tsmsf1o  24093  xmetgt0  24306  txmetcnp  24495  metustsym  24503  nlmmul0or  24631  cnmet  24719  evth  24918  isclmp  25057  minveclem3b  25388  mbfposr  25613  itg2cn  25724  iblcnlem  25750  dvcvx  25985  ulm2  26354  efeq1  26497  dcubic  26816  mcubic  26817  dquart  26823  birthdaylem3  26923  ftalem2  27044  issqf  27106  sqff1o  27152  bposlem7  27261  lgsabs1  27307  gausslemma2dlem1a  27336  lgsquadlem2  27352  addsq2reu  27411  dchrisum0lem1  27487  ssltsnb  27769  sltrec  27799  opphllem6  28807  colhp  28825  lmiinv  28847  lmiopp  28857  wlkeq  29690  eupth2lem3lem3  30288  eupth2lem3lem6  30291  nmounbi  30834  ip2eqi  30914  hvmulcan  31130  hvsubcan2  31133  hi2eq  31163  fh2  31677  riesz4i  32121  cvbr4i  32425  sgnmulsgn  32904  sgnmulsgp  32905  xdivpnfrp  32995  qusker  33411  ellspds  33430  ply1moneq  33650  ballotlemfc0  34631  ballotlemfcc  34632  subfacp1lem5  35359  topfneec2  36531  neibastop3  36537  unccur  37775  cos2h  37783  tan2h  37784  poimirlem25  37817  poimirlem27  37819  dvasin  37876  caures  37932  ismtyima  37975  isdmn3  38246  dmecd  38482  releldmqscoss  38917  tendospcanN  41320  dochsncom  41679  f1o2d2  42526  sqrtcval  43918  or3or  44300  neicvgel1  44396  rusbcALT  44715  sbcoreleleqVD  45135  climreeq  45895  coseq0  46144  modmkpkne  47643  affinecomb1  48984  eenglngeehlnmlem1  49019  2sphere  49031  line2  49034  itscnhlc0yqe  49041  itscnhlc0xyqsol  49047  oduoppcciso  49847