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  4363  fnprb  7137  fntpb  7138  eqfunresadj  7289  eloprabga  7450  ordsucuniel  7749  ordsucun  7750  oeoa  8507  ereldm  8670  boxcutc  8860  mapen  9049  mapfien  9287  wemapwe  9582  sdom2en01  10185  prlem936  10930  subcan  11408  mulcan1g  11762  conjmul  11830  ltrec  11996  rebtwnz  12837  xposdif  13153  divelunit  13386  fseq1m1p1  13491  fzm1  13499  fllt  13702  hashfacen  14353  hashf1  14356  ccat0  14475  lenegsq  15220  dvdsmod  16232  bitsmod  16339  smueqlem  16393  rpexp  16625  eulerthlem2  16685  odzdvds  16699  pcelnn  16774  xpsle  17475  isepi  17639  fthmon  17828  cat1  17996  pospropd  18223  grpidpropd  18562  mgmhmpropd  18598  sgrppropd  18631  mndpropd  18659  mhmpropd  18692  grppropd  18856  ghmnsgima  19145  mndodcong  19447  odf1  19467  odf1o1  19477  sylow3lem6  19537  lsmcntzr  19585  efgredlema  19645  cmnpropd  19696  qusecsub  19740  dprdf11  19930  rngpropd  20085  ringpropd  20199  dvdsrpropd  20327  resrhm2b  20510  abvpropd  20743  isorng  20769  lmodprop2d  20850  lsspropd  20944  lmhmpropd  21000  lbspropd  21026  lvecvscan  21041  lvecvscan2  21042  chrnzr  21460  zndvds0  21480  ip2eq  21583  phlpropd  21585  assapropd  21802  qtopcn  23622  tsmsf1o  24053  xmetgt0  24266  txmetcnp  24455  metustsym  24463  nlmmul0or  24591  cnmet  24679  evth  24878  isclmp  25017  minveclem3b  25348  mbfposr  25573  itg2cn  25684  iblcnlem  25710  dvcvx  25945  ulm2  26314  efeq1  26457  dcubic  26776  mcubic  26777  dquart  26783  birthdaylem3  26883  ftalem2  27004  issqf  27066  sqff1o  27112  bposlem7  27221  lgsabs1  27267  gausslemma2dlem1a  27296  lgsquadlem2  27312  addsq2reu  27371  dchrisum0lem1  27447  ssltsnb  27725  sltrec  27755  opphllem6  28723  colhp  28741  lmiinv  28763  lmiopp  28773  wlkeq  29605  eupth2lem3lem3  30200  eupth2lem3lem6  30203  nmounbi  30746  ip2eqi  30826  hvmulcan  31042  hvsubcan2  31045  hi2eq  31075  fh2  31589  riesz4i  32033  cvbr4i  32337  sgnmulsgn  32815  sgnmulsgp  32816  xdivpnfrp  32903  qusker  33304  ellspds  33323  ply1moneq  33540  ballotlemfc0  34496  ballotlemfcc  34497  subfacp1lem5  35196  topfneec2  36369  neibastop3  36375  unccur  37622  cos2h  37630  tan2h  37631  poimirlem25  37664  poimirlem27  37666  dvasin  37723  caures  37779  ismtyima  37822  isdmn3  38093  dmecd  38317  releldmqscoss  38677  tendospcanN  41041  dochsncom  41400  f1o2d2  42245  sqrtcval  43653  or3or  44035  neicvgel1  44131  rusbcALT  44450  sbcoreleleqVD  44870  climreeq  45632  coseq0  45881  modmkpkne  47371  affinecomb1  48713  eenglngeehlnmlem1  48748  2sphere  48760  line2  48763  itscnhlc0yqe  48770  itscnhlc0xyqsol  48776  oduoppcciso  49577