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  3163  eloprabga  6142  ereldm  6814  mapen  7101  ordiso2  7328  subcan  8533  conjmulap  9008  ltrec  9162  divelunit  10341  fseq1m1p1  10436  fzm1  10441  qsqeqor  11019  fihashneq0  11165  hashfacen  11216  ccat0  11292  cvg1nlemcau  11677  lenegsq  11788  dvdsmod  12556  bitsmod  12650  bezoutlemle  12712  rpexp  12858  qnumdenbi  12897  eulerthlemh  12936  odzdvds  12951  pcelnn  13027  ballotfilemfc0  13157  ballotfilemfcc  13158  grpidpropdg  13608  sgrppropd  13647  mndpropd  13674  mhmpropd  13700  grppropd  13751  ghmnsgima  14006  cmnpropd  14033  qusecsub  14069  rngpropd  14120  ringpropd  14203  dvdsrpropdg  14314  resrhm2b  14417  opprdrng  14480  lmodprop2d  14545  lsspropdg  14628  zndvds0  14847  bdxmet  15415  txmetcnp  15432  cnmet  15444  lgsne0  15960  lgsabs1  15961  gausslemma2dlem1a  15980  lgsquadlem2  16000  usgredg2v  16268  wlkeq  16398  eupth2lem3lem3fi  16514  eupth2lem3lem6fi  16515