Theorem 3bitr3d 218

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

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  csbcomg  3148  eloprabga  6103  ereldm  6742  mapen  7027  ordiso2  7228  subcan  8427  conjmulap  8902  ltrec  9056  divelunit  10230  fseq1m1p1  10323  fzm1  10328  qsqeqor  10905  fihashneq0  11049  hashfacen  11093  ccat0  11166  cvg1nlemcau  11538  lenegsq  11649  dvdsmod  12416  bitsmod  12510  bezoutlemle  12572  rpexp  12718  qnumdenbi  12757  eulerthlemh  12796  odzdvds  12811  pcelnn  12887  grpidpropdg  13450  sgrppropd  13489  mndpropd  13516  mhmpropd  13542  grppropd  13593  ghmnsgima  13848  cmnpropd  13875  qusecsub  13911  rngpropd  13961  ringpropd  14044  dvdsrpropdg  14154  resrhm2b  14256  lmodprop2d  14355  lsspropdg  14438  zndvds0  14657  bdxmet  15218  txmetcnp  15235  cnmet  15247  lgsne0  15760  lgsabs1  15761  gausslemma2dlem1a  15780  lgsquadlem2  15800  usgredg2v  16068  wlkeq  16165