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  3147  eloprabga  6097  ereldm  6733  mapen  7015  ordiso2  7210  subcan  8409  conjmulap  8884  ltrec  9038  divelunit  10206  fseq1m1p1  10299  fzm1  10304  qsqeqor  10880  fihashneq0  11024  hashfacen  11066  ccat0  11139  cvg1nlemcau  11503  lenegsq  11614  dvdsmod  12381  bitsmod  12475  bezoutlemle  12537  rpexp  12683  qnumdenbi  12722  eulerthlemh  12761  odzdvds  12776  pcelnn  12852  grpidpropdg  13415  sgrppropd  13454  mndpropd  13481  mhmpropd  13507  grppropd  13558  ghmnsgima  13813  cmnpropd  13840  qusecsub  13876  rngpropd  13926  ringpropd  14009  dvdsrpropdg  14119  resrhm2b  14221  lmodprop2d  14320  lsspropdg  14403  zndvds0  14622  bdxmet  15183  txmetcnp  15200  cnmet  15212  lgsne0  15725  lgsabs1  15726  gausslemma2dlem1a  15745  lgsquadlem2  15765  usgredg2v  16030  wlkeq  16075