Theorem 3bitr2d 216

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr2d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr2d.2	⊢ (𝜑 → (𝜃 ↔ 𝜒))
3bitr2d.3	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
3bitr2d	⊢ (𝜑 → (𝜓 ↔ 𝜏))

Proof of Theorem 3bitr2d

Step	Hyp	Ref	Expression
1		3bitr2d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		3bitr2d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	1, 2	bitr4d 191	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.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:  ceqsralt  2764  frecsuclem  6400  indpi  7319  cauappcvgprlemladdru  7633  prsrlt  7764  lesub2  8391  ltsub2  8393  rec11ap  8643  avglt1  9133  rpnegap  9660  modqmuladdnn0  10341  expap0  10523  2shfti  10811  mulreap  10844  minmax  11209  lemininf  11213  xrminmax  11244  xrlemininf  11250  modremain  11904  nn0seqcvgd  12011  divgcdcoprm0  12071  ismgmid  12675  grpsubeq0  12832  grpsubadd  12834  isunitd  13087  isxmet2d  13481  xblss2  13538  neibl  13624  ellimc3apf  13762  logbgt0b  14017  lgsne0  14072  lgsabs1  14073  iswomninnlem  14420