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  4438  fnprb  7245  fntpb  7246  eqfunresadj  7396  eloprabga  7558  eloprabgaOLD  7559  ordsucuniel  7860  ordsucun  7861  oeoa  8653  ereldm  8813  boxcutc  8999  mapen  9207  mapfien  9477  wemapwe  9766  sdom2en01  10371  prlem936  11116  subcan  11591  mulcan1g  11943  conjmul  12011  ltrec  12177  rebtwnz  13012  xposdif  13324  divelunit  13554  fseq1m1p1  13659  fzm1  13664  fllt  13857  hashfacen  14503  hashf1  14506  ccat0  14624  lenegsq  15369  dvdsmod  16377  bitsmod  16482  smueqlem  16536  rpexp  16769  eulerthlem2  16829  odzdvds  16842  pcelnn  16917  xpsle  17639  isepi  17801  fthmon  17994  cat1  18164  pospropd  18397  grpidpropd  18700  mgmhmpropd  18736  sgrppropd  18769  mndpropd  18797  mhmpropd  18827  grppropd  18991  ghmnsgima  19280  mndodcong  19584  odf1  19604  odf1o1  19614  sylow3lem6  19674  lsmcntzr  19722  efgredlema  19782  cmnpropd  19833  qusecsub  19877  dprdf11  20067  rngpropd  20201  ringpropd  20311  dvdsrpropd  20442  resrhm2b  20630  abvpropd  20858  lmodprop2d  20944  lsspropd  21039  lmhmpropd  21095  lbspropd  21121  lvecvscan  21136  lvecvscan2  21137  chrnzr  21568  zndvds0  21592  ip2eq  21694  phlpropd  21696  assapropd  21915  qtopcn  23743  tsmsf1o  24174  xmetgt0  24389  txmetcnp  24581  metustsym  24589  nlmmul0or  24725  cnmet  24813  evth  25010  isclmp  25149  minveclem3b  25481  mbfposr  25706  itg2cn  25818  iblcnlem  25844  dvcvx  26079  ulm2  26446  efeq1  26588  dcubic  26907  mcubic  26908  dquart  26914  birthdaylem3  27014  ftalem2  27135  issqf  27197  sqff1o  27243  bposlem7  27352  lgsabs1  27398  gausslemma2dlem1a  27427  lgsquadlem2  27443  addsq2reu  27502  dchrisum0lem1  27578  sltrec  27883  opphllem6  28778  colhp  28796  lmiinv  28818  lmiopp  28828  wlkeq  29670  eupth2lem3lem3  30262  eupth2lem3lem6  30265  nmounbi  30808  ip2eqi  30888  hvmulcan  31104  hvsubcan2  31107  hi2eq  31137  fh2  31651  riesz4i  32095  cvbr4i  32399  xdivpnfrp  32897  isorng  33294  qusker  33342  ellspds  33361  ply1moneq  33576  ballotlemfc0  34457  ballotlemfcc  34458  sgnmulsgn  34514  sgnmulsgp  34515  subfacp1lem5  35152  topfneec2  36322  neibastop3  36328  unccur  37563  cos2h  37571  tan2h  37572  poimirlem25  37605  poimirlem27  37607  dvasin  37664  caures  37720  ismtyima  37763  isdmn3  38034  dmecd  38260  releldmqscoss  38616  tendospcanN  40980  dochsncom  41339  f1o2d2  42228  sqrtcval  43603  or3or  43985  neicvgel1  44081  rusbcALT  44408  sbcoreleleqVD  44830  climreeq  45534  coseq0  45785  affinecomb1  48436  eenglngeehlnmlem1  48471  2sphere  48483  line2  48486  itscnhlc0yqe  48493  itscnhlc0xyqsol  48499