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  3170  eloprabga  6169  ereldm  6846  mapen  7140  ordiso2  7369  subcan  8575  conjmulap  9053  ltrec  9207  divelunit  10387  fseq1m1p1  10485  fzm1  10490  qsqeqor  11070  fihashneq0  11216  hashfacen  11267  hashf1  11270  ccat0  11347  cvg1nlemcau  11733  lenegsq  11844  dvdsmod  12612  bitsmod  12706  bezoutlemle  12768  rpexp  12914  qnumdenbi  12953  eulerthlemh  12992  odzdvds  13007  pcelnn  13083  ballotfilemfc0  13215  ballotfilemfcc  13216  grpidpropdg  13677  sgrppropd  13711  mndpropd  13736  mhmpropd  13756  grppropd  13805  ghmnsgima  14054  cmnpropd  14081  qusecsub  14118  rngpropd  14237  ringpropd  14326  dvdsrpropdg  14437  resrhm2b  14540  opprdrng  14603  lmodprop2d  14668  lsspropdg  14751  zndvds0  14968  assapropd  14997  bdxmet  15585  txmetcnp  15602  cnmet  15614  birthdaylem3  16072  lgsne0  16140  lgsabs1  16141  gausslemma2dlem1a  16160  lgsquadlem2  16180  usgredg2v  16448  wlkeq  16578  eupth2lem3lem3fi  16694  eupth2lem3lem6fi  16695