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  6100  ereldm  6738  mapen  7020  ordiso2  7218  subcan  8417  conjmulap  8892  ltrec  9046  divelunit  10215  fseq1m1p1  10308  fzm1  10313  qsqeqor  10889  fihashneq0  11033  hashfacen  11076  ccat0  11149  cvg1nlemcau  11516  lenegsq  11627  dvdsmod  12394  bitsmod  12488  bezoutlemle  12550  rpexp  12696  qnumdenbi  12735  eulerthlemh  12774  odzdvds  12789  pcelnn  12865  grpidpropdg  13428  sgrppropd  13467  mndpropd  13494  mhmpropd  13520  grppropd  13571  ghmnsgima  13826  cmnpropd  13853  qusecsub  13889  rngpropd  13939  ringpropd  14022  dvdsrpropdg  14132  resrhm2b  14234  lmodprop2d  14333  lsspropdg  14416  zndvds0  14635  bdxmet  15196  txmetcnp  15213  cnmet  15225  lgsne0  15738  lgsabs1  15739  gausslemma2dlem1a  15758  lgsquadlem2  15778  usgredg2v  16043  wlkeq  16126