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  4352  fnprb  7116  fntpb  7117  eloprabga  7414  eloprabgaOLD  7415  ordsucuniel  7703  ordsucun  7704  oeoa  8459  ereldm  8577  boxcutc  8760  mapen  8966  mapfien  9211  wemapwe  9499  sdom2en01  10104  prlem936  10849  subcan  11322  mulcan1g  11674  conjmul  11738  ltrec  11903  rebtwnz  12733  xposdif  13042  divelunit  13272  fseq1m1p1  13377  fzm1  13382  fllt  13572  hashfacen  14211  hashfacenOLD  14212  hashf1  14216  ccat0  14325  lenegsq  15077  dvdsmod  16083  bitsmod  16188  smueqlem  16242  rpexp  16472  eulerthlem2  16528  odzdvds  16541  pcelnn  16616  xpsle  17335  isepi  17497  fthmon  17688  cat1  17857  pospropd  18090  grpidpropd  18391  mndpropd  18455  mhmpropd  18481  grppropd  18639  ghmnsgima  18903  mndodcong  19195  odf1  19214  odf1o1  19222  sylow3lem6  19282  lsmcntzr  19331  efgredlema  19391  cmnpropd  19441  dprdf11  19671  ringpropd  19866  dvdsrpropd  19983  abvpropd  20147  lmodprop2d  20230  lsspropd  20324  lmhmpropd  20380  lbspropd  20406  lvecvscan  20418  lvecvscan2  20419  chrnzr  20779  zndvds0  20803  ip2eq  20903  phlpropd  20905  assapropd  21121  qtopcn  22910  tsmsf1o  23341  xmetgt0  23556  txmetcnp  23748  metustsym  23756  nlmmul0or  23892  cnmet  23980  evth  24167  isclmp  24305  minveclem3b  24637  mbfposr  24861  itg2cn  24973  iblcnlem  24998  dvcvx  25229  ulm2  25589  efeq1  25729  dcubic  26041  mcubic  26042  dquart  26048  birthdaylem3  26148  ftalem2  26268  issqf  26330  sqff1o  26376  bposlem7  26483  lgsabs1  26529  gausslemma2dlem1a  26558  lgsquadlem2  26574  addsq2reu  26633  dchrisum0lem1  26709  opphllem6  27158  colhp  27176  lmiinv  27198  lmiopp  27208  wlkeq  28046  eupth2lem3lem3  28639  eupth2lem3lem6  28642  nmounbi  29183  ip2eqi  29263  hvmulcan  29479  hvsubcan2  29482  hi2eq  29512  fh2  30026  riesz4i  30470  cvbr4i  30774  xdivpnfrp  31252  isorng  31543  qusker  31594  ellspds  31609  ballotlemfc0  32504  ballotlemfcc  32505  sgnmulsgn  32561  sgnmulsgp  32562  subfacp1lem5  33191  eqfunresadj  33780  sltrec  34059  topfneec2  34590  neibastop3  34596  unccur  35804  cos2h  35812  tan2h  35813  poimirlem25  35846  poimirlem27  35848  dvasin  35905  caures  35962  ismtyima  36005  isdmn3  36276  dmecd  36482  releldmqscoss  36814  tendospcanN  39079  dochsncom  39438  sqrtcval  41287  or3or  41669  neicvgel1  41767  rusbcALT  42095  sbcoreleleqVD  42517  climreeq  43203  coseq0  43454  mgmhmpropd  45397  affinecomb1  46106  eenglngeehlnmlem1  46141  2sphere  46153  line2  46156  itscnhlc0yqe  46163  itscnhlc0xyqsol  46169