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  6010  ereldm  6638  mapen  6908  ordiso2  7102  subcan  8283  conjmulap  8758  ltrec  8912  divelunit  10079  fseq1m1p1  10172  fzm1  10177  qsqeqor  10744  fihashneq0  10888  hashfacen  10930  cvg1nlemcau  11151  lenegsq  11262  dvdsmod  12029  bitsmod  12123  bezoutlemle  12185  rpexp  12331  qnumdenbi  12370  eulerthlemh  12409  odzdvds  12424  pcelnn  12500  grpidpropdg  13027  sgrppropd  13066  mndpropd  13091  mhmpropd  13108  grppropd  13159  ghmnsgima  13408  cmnpropd  13435  qusecsub  13471  rngpropd  13521  ringpropd  13604  dvdsrpropdg  13713  resrhm2b  13815  lmodprop2d  13914  lsspropdg  13997  zndvds0  14216  bdxmet  14747  txmetcnp  14764  cnmet  14776  lgsne0  15289  lgsabs1  15290  gausslemma2dlem1a  15309  lgsquadlem2  15329