Theorem 3bitr3d 312

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 284	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr3d.3	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜏))
5	3, 4	bitrd 282	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  sbcne12  4376  fnprb  7211  fntpb  7212  eqfunresadj  7367  eloprabga  7526  ordsucuniel  7824  ordsucun  7825  mpof1o2d  8127  oeoa  8589  ereldm  8754  boxcutc  8952  mapen  9143  mapfien  9382  wemapwe  9680  sdom2en01  10308  prlem936  11060  subcan  11541  mulcan1g  11895  conjmul  11960  ltrec  12125  rebtwnz  13000  xposdif  13318  divelunit  13551  fseq1m1p1  13658  fzm1  13666  fllt  13871  hashfacen  14523  hashf1  14526  ccat0  14645  sgnmulsgn  15186  lenegsq  15412  dvdsmod  16425  bitsmod  16532  smueqlem  16586  rpexp  16819  eulerthlem2  16879  odzdvds  16893  pcelnn  16968  xpsle  17671  isepi  17835  fthmon  18024  cat1  18192  pospropd  18419  grpidpropd  18761  mgmhmpropd  18806  sgrppropd  18839  mndpropd  18870  mhmpropd  18906  grppropd  19081  ghmnsgima  19373  mndodcong  19675  odf1  19695  odf1o1  19705  sylow3lem6  19765  lsmcntzr  19813  efgredlema  19873  cmnpropd  19924  qusecsub  19968  dprdf11  20158  rngpropd  20315  ringpropd  20436  dvdsrpropd  20563  resrhm2b  20770  abvpropd  21007  isorng  21033  lmodprop2d  21114  lsspropd  21207  lmhmpropd  21263  lbspropd  21289  lvecvscan  21304  lvecvscan2  21305  chrnzr  21749  zndvds0  21769  ip2eq  21872  phlpropd  21874  assapropd  22092  qtopcn  23946  tsmsf1o  24377  xmetgt0  24590  txmetcnp  24779  metustsym  24787  nlmmul0or  24915  cnmet  25003  evth  25193  isclmp  25331  minveclem3b  25662  mbfposr  25886  itg2cn  25997  iblcnlem  26023  dvcvx  26254  ulm2  26628  efeq1  26773  dcubic  27091  mcubic  27092  dquart  27098  birthdaylem3  27198  ftalem2  27318  issqf  27380  sqff1o  27426  bposlem7  27534  lgsabs1  27580  gausslemma2dlem1a  27609  lgsquadlem2  27625  addsq2reu  27684  dchrisum0lem1  27760  sltssnb  28042  ltsrec  28074  opphllem6  29115  colhp  29135  lmiinv  29184  lmiopp  29195  wlkeq  30101  eupth2lem3lem3  30718  eupth2lem3lem6  30721  nmounbi  31265  ip2eqi  31345  hvmulcan  31561  hvsubcan2  31564  hi2eq  31594  fh2  32108  riesz4i  32552  cvbr4i  32856  sgnmulsgp  33310  xdivpnfrp  33386  qusker  33797  ellspds  33811  ply1moneq  34006  ballotlemfc0  35012  ballotlemfcc  35013  subfacp1lem5  35771  topfneec2  36983  neibastop3  36989  unccur  38365  cos2h  38373  tan2h  38374  poimirlem25  38402  poimirlem27  38404  dvasin  38461  caures  38518  ismtyima  38561  isdmn3  38832  dmecd  39066  releldmqscoss  39501  tendospcanN  41904  dochsncom  42263  quadfac  43079  sqrtcval  44489  or3or  44871  neicvgel1  44967  rusbcALT  45270  sbcoreleleqVD  45689  climreeq  46451  coseq0  46700  modmkpkne  48263  isidom3  49268  affinecomb1  49640  eenglngeehlnmlem1  49675  2sphere  49687  line2  49690  itscnhlc0yqe  49697  itscnhlc0xyqsol  49703  oduoppcciso  50500