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  3107  eloprabga  6013  ereldm  6646  mapen  6916  ordiso2  7110  subcan  8300  conjmulap  8775  ltrec  8929  divelunit  10096  fseq1m1p1  10189  fzm1  10194  qsqeqor  10761  fihashneq0  10905  hashfacen  10947  cvg1nlemcau  11168  lenegsq  11279  dvdsmod  12046  bitsmod  12140  bezoutlemle  12202  rpexp  12348  qnumdenbi  12387  eulerthlemh  12426  odzdvds  12441  pcelnn  12517  grpidpropdg  13078  sgrppropd  13117  mndpropd  13144  mhmpropd  13170  grppropd  13221  ghmnsgima  13476  cmnpropd  13503  qusecsub  13539  rngpropd  13589  ringpropd  13672  dvdsrpropdg  13781  resrhm2b  13883  lmodprop2d  13982  lsspropdg  14065  zndvds0  14284  bdxmet  14823  txmetcnp  14840  cnmet  14852  lgsne0  15365  lgsabs1  15366  gausslemma2dlem1a  15385  lgsquadlem2  15405