Theorem 3bitr3d 308

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 280	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3d.3	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜏))
5	3, 4	bitrd 278	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  4377  fnprb  7163  fntpb  7164  eqfunresadj  7310  eloprabga  7469  eloprabgaOLD  7470  ordsucuniel  7764  ordsucun  7765  oeoa  8549  ereldm  8703  boxcutc  8886  mapen  9092  mapfien  9353  wemapwe  9642  sdom2en01  10247  prlem936  10992  subcan  11465  mulcan1g  11817  conjmul  11881  ltrec  12046  rebtwnz  12881  xposdif  13191  divelunit  13421  fseq1m1p1  13526  fzm1  13531  fllt  13721  hashfacen  14363  hashfacenOLD  14364  hashf1  14368  ccat0  14476  lenegsq  15217  dvdsmod  16222  bitsmod  16327  smueqlem  16381  rpexp  16609  eulerthlem2  16665  odzdvds  16678  pcelnn  16753  xpsle  17475  isepi  17637  fthmon  17828  cat1  17997  pospropd  18230  grpidpropd  18531  mndpropd  18595  mhmpropd  18622  grppropd  18779  ghmnsgima  19046  mndodcong  19338  odf1  19358  odf1o1  19368  sylow3lem6  19428  lsmcntzr  19476  efgredlema  19536  cmnpropd  19587  dprdf11  19816  ringpropd  20020  dvdsrpropd  20141  resrhm2b  20301  abvpropd  20357  lmodprop2d  20441  lsspropd  20535  lmhmpropd  20591  lbspropd  20617  lvecvscan  20631  lvecvscan2  20632  chrnzr  20970  zndvds0  20994  ip2eq  21094  phlpropd  21096  assapropd  21312  qtopcn  23102  tsmsf1o  23533  xmetgt0  23748  txmetcnp  23940  metustsym  23948  nlmmul0or  24084  cnmet  24172  evth  24359  isclmp  24497  minveclem3b  24829  mbfposr  25053  itg2cn  25165  iblcnlem  25190  dvcvx  25421  ulm2  25781  efeq1  25921  dcubic  26233  mcubic  26234  dquart  26240  birthdaylem3  26340  ftalem2  26460  issqf  26522  sqff1o  26568  bposlem7  26675  lgsabs1  26721  gausslemma2dlem1a  26750  lgsquadlem2  26766  addsq2reu  26825  dchrisum0lem1  26901  sltrec  27202  opphllem6  27757  colhp  27775  lmiinv  27797  lmiopp  27807  wlkeq  28645  eupth2lem3lem3  29237  eupth2lem3lem6  29240  nmounbi  29781  ip2eqi  29861  hvmulcan  30077  hvsubcan2  30080  hi2eq  30110  fh2  30624  riesz4i  31068  cvbr4i  31372  xdivpnfrp  31859  isorng  32165  qusker  32212  ellspds  32229  ply1moneq  32364  ballotlemfc0  33181  ballotlemfcc  33182  sgnmulsgn  33238  sgnmulsgp  33239  subfacp1lem5  33865  topfneec2  34904  neibastop3  34910  unccur  36134  cos2h  36142  tan2h  36143  poimirlem25  36176  poimirlem27  36178  dvasin  36235  caures  36292  ismtyima  36335  isdmn3  36606  dmecd  36838  releldmqscoss  37195  tendospcanN  39559  dochsncom  39918  sqrtcval  42035  or3or  42417  neicvgel1  42513  rusbcALT  42841  sbcoreleleqVD  43263  climreeq  43974  coseq0  44225  mgmhmpropd  46199  affinecomb1  46908  eenglngeehlnmlem1  46943  2sphere  46955  line2  46958  itscnhlc0yqe  46965  itscnhlc0xyqsol  46971