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 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  sbcne12  4379  fnprb  7206  fntpb  7207  eqfunresadj  7358  eloprabga  7519  ordsucuniel  7819  ordsucun  7820  mpof1o2d  8120  oeoa  8582  ereldm  8747  boxcutc  8938  mapen  9128  mapfien  9367  wemapwe  9665  sdom2en01  10285  prlem936  11031  subcan  11512  mulcan1g  11866  conjmul  11931  ltrec  12096  rebtwnz  12970  xposdif  13287  divelunit  13520  fseq1m1p1  13627  fzm1  13635  fllt  13839  hashfacen  14491  hashf1  14494  ccat0  14613  sgnmulsgn  15146  lenegsq  15372  dvdsmod  16386  bitsmod  16493  smueqlem  16547  rpexp  16780  eulerthlem2  16840  odzdvds  16854  pcelnn  16929  xpsle  17632  isepi  17796  fthmon  17985  cat1  18153  pospropd  18380  grpidpropd  18719  mgmhmpropd  18755  sgrppropd  18788  mndpropd  18816  mhmpropd  18849  grppropd  19017  ghmnsgima  19309  mndodcong  19611  odf1  19631  odf1o1  19641  sylow3lem6  19701  lsmcntzr  19749  efgredlema  19809  cmnpropd  19860  qusecsub  19904  dprdf11  20094  rngpropd  20251  ringpropd  20370  dvdsrpropd  20497  resrhm2b  20686  abvpropd  20917  isorng  20943  lmodprop2d  21024  lsspropd  21117  lmhmpropd  21173  lbspropd  21199  lvecvscan  21214  lvecvscan2  21215  chrnzr  21659  zndvds0  21679  ip2eq  21782  phlpropd  21784  assapropd  22000  qtopcn  23850  tsmsf1o  24281  xmetgt0  24494  txmetcnp  24683  metustsym  24691  nlmmul0or  24819  cnmet  24907  evth  25097  isclmp  25235  minveclem3b  25566  mbfposr  25790  itg2cn  25901  iblcnlem  25927  dvcvx  26158  ulm2  26524  efeq1  26669  dcubic  26987  mcubic  26988  dquart  26994  birthdaylem3  27094  ftalem2  27214  issqf  27276  sqff1o  27322  bposlem7  27430  lgsabs1  27476  gausslemma2dlem1a  27505  lgsquadlem2  27521  addsq2reu  27580  dchrisum0lem1  27656  sltssnb  27938  ltsrec  27970  opphllem6  29008  colhp  29027  lmiinv  29075  lmiopp  29085  wlkeq  29949  eupth2lem3lem3  30547  eupth2lem3lem6  30550  nmounbi  31094  ip2eqi  31174  hvmulcan  31390  hvsubcan2  31393  hi2eq  31423  fh2  31937  riesz4i  32381  cvbr4i  32685  sgnmulsgp  33142  xdivpnfrp  33218  qusker  33635  ellspds  33649  ply1moneq  33844  ballotlemfc0  34849  ballotlemfcc  34850  subfacp1lem5  35642  topfneec2  36833  neibastop3  36839  unccur  38220  cos2h  38228  tan2h  38229  poimirlem25  38262  poimirlem27  38264  dvasin  38321  caures  38377  ismtyima  38420  isdmn3  38691  dmecd  38927  releldmqscoss  39362  tendospcanN  41765  dochsncom  42124  quadfac  42940  sqrtcval  44337  or3or  44719  neicvgel1  44815  rusbcALT  45118  sbcoreleleqVD  45537  climreeq  46299  coseq0  46548  modmkpkne  48071  isidom3  49077  affinecomb1  49449  eenglngeehlnmlem1  49484  2sphere  49496  line2  49499  itscnhlc0yqe  49506  itscnhlc0xyqsol  49512  oduoppcciso  50311