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  2766  frecsuclem  6409  indpi  7343  cauappcvgprlemladdru  7657  prsrlt  7788  lesub2  8416  ltsub2  8418  rec11ap  8669  avglt1  9159  rpnegap  9688  modqmuladdnn0  10370  expap0  10552  2shfti  10842  mulreap  10875  minmax  11240  lemininf  11244  xrminmax  11275  xrlemininf  11281  modremain  11936  nn0seqcvgd  12043  divgcdcoprm0  12103  ismgmid  12801  grpsubeq0  12961  grpsubadd  12963  isunitd  13280  lsslss  13473  isxmet2d  13887  xblss2  13944  neibl  14030  ellimc3apf  14168  logbgt0b  14423  lgsne0  14478  lgsabs1  14479  m1lgs  14491  iswomninnlem  14836