Theorem 3bitr2d 215

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 190	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 187	1 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ceqsralt  2716  frecsuclem  6311  indpi  7174  cauappcvgprlemladdru  7488  prsrlt  7619  lesub2  8243  ltsub2  8245  rec11ap  8494  avglt1  8982  rpnegap  9503  modqmuladdnn0  10172  expap0  10354  2shfti  10635  mulreap  10668  minmax  11033  lemininf  11037  xrminmax  11066  xrlemininf  11072  modremain  11662  nn0seqcvgd  11758  divgcdcoprm0  11818  isxmet2d  12556  xblss2  12613  neibl  12699  ellimc3apf  12837  logbgt0b  13091  iswomninnlem  13417