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  3092  eloprabga  5975  ereldm  6592  mapen  6860  ordiso2  7048  subcan  8226  conjmulap  8700  ltrec  8854  divelunit  10016  fseq1m1p1  10109  fzm1  10114  qsqeqor  10645  fihashneq0  10788  hashfacen  10830  cvg1nlemcau  11007  lenegsq  11118  dvdsmod  11882  bezoutlemle  12023  rpexp  12167  qnumdenbi  12206  eulerthlemh  12245  odzdvds  12259  pcelnn  12334  grpidpropdg  12812  sgrppropd  12838  mndpropd  12863  mhmpropd  12879  grppropd  12915  cmnpropd  13132  qusecsub  13166  rngpropd  13207  ringpropd  13290  dvdsrpropdg  13395  lmodprop2d  13537  lsspropdg  13620  bdxmet  14297  txmetcnp  14314  cnmet  14326  lgsne0  14735  lgsabs1  14736