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  3160  eloprabga  6139  ereldm  6811  mapen  7098  ordiso2  7325  subcan  8524  conjmulap  8999  ltrec  9153  divelunit  10331  fseq1m1p1  10425  fzm1  10430  qsqeqor  11008  fihashneq0  11152  hashfacen  11201  ccat0  11277  cvg1nlemcau  11662  lenegsq  11773  dvdsmod  12541  bitsmod  12635  bezoutlemle  12697  rpexp  12843  qnumdenbi  12882  eulerthlemh  12921  odzdvds  12936  pcelnn  13012  grpidpropdg  13576  sgrppropd  13615  mndpropd  13642  mhmpropd  13668  grppropd  13719  ghmnsgima  13974  cmnpropd  14001  qusecsub  14037  rngpropd  14088  ringpropd  14171  dvdsrpropdg  14281  resrhm2b  14383  lmodprop2d  14483  lsspropdg  14566  zndvds0  14785  bdxmet  15353  txmetcnp  15370  cnmet  15382  lgsne0  15898  lgsabs1  15899  gausslemma2dlem1a  15918  lgsquadlem2  15938  usgredg2v  16206  wlkeq  16336  eupth2lem3lem3fi  16452  eupth2lem3lem6fi  16453